let R be Ring; :: thesis: 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
let X, Y be LeftMod of R; :: thesis: 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
let X0 be Subset of X; :: thesis: 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
let L be linear-transformation of X,Y; :: thesis: for l being Linear_Combination of L .: X0 st X0 = the carrier of X & L is one-to-one holds
L # l = l * L
let l be Linear_Combination of L .: X0; :: thesis: ( X0 = the carrier of X & L is one-to-one implies L # l = l * L )
assume that
A0: X0 = the carrier of X and
A1: L is one-to-one ; :: thesis: L # l = l * L
X1: L | X0 is one-to-one by A1, FUNCT_1:52;
X3: X0 ` = {} by XBOOLE_1:37, A0;
L # l = (l * L) +* ({} --> (0. R)) by X3, X1, ZMODUL05:def 9
.= l * L ;
hence L # l = l * L ; :: thesis: verum