theorem Th39: :: ZMODUL05:56
for R being Ring
for V, W being LeftMod of R
for l being Linear_Combination of V
for T being linear-transformation of V,W st T | (Carrier l) is one-to-one holds
T .: (Carrier l) = Carrier (T @* l)