theorem :: ZMODUL05:51

for R being Ring
for V, W being LeftMod of R
for A being Subset of V
for l being Linear_Combination of A
for T being linear-transformation of V,W
for v being Element of V st T | A is one-to-one & v in A holds
ex X being Subset of V st
( X misses A & T " {(T . v)} = {v} \/ X )