theorem :: ZMODUL06:44

for R being Ring
for X, Y being LeftMod of R
for X0 being Subset of X
for L being linear-transformation of X,Y
for l being Linear_Combination of L .: X0 st X0 = the carrier of X & L is one-to-one holds
L # l = l * L