∀ {R : Type u_1} {N : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (f i : N →ₗ[R] M) (K : Submodule R N) (m : ℕ),
  f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K →
    Function.Surjective ⇑f → Function.Injective ⇑i → ∀ (n : ℕ), f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K