theorem :: ZMODUL05:60

for V, W being Z_Module
for T being linear-transformation of V,W
for X being Subset of V
for l being Linear_Combination of T .: X st T | X is one-to-one holds
T @* (T # l) = l