∀ {R : Type u_2} {M : Type u_1} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_3}
  [inst_3 : DecidableEq ι] {N : ι → Submodule R M} (ind : iSupIndep N) (iSup_top : ⨆ i, N i = ⊤)
  (invar : ∀ (i : ι), (N i).IsFullyInvariant) (f : Module.End R M) (x : M),
  ((fun f => ↑(ind.linearEquiv iSup_top) ∘ₗ DFinsupp.mapRange.linearMap f ∘ₗ ↑(ind.linearEquiv iSup_top).symm)
        ((fun f i => LinearMap.restrict f ⋯) f))
      x =
    f x