let R be Ring; :: thesis: for X, Y being LeftMod of R
for l being Linear_Combination of X
for L being linear-transformation of X,Y st L is bijective holds
L @* l = l * (L ")
let X, Y be LeftMod of R; :: thesis: for l being Linear_Combination of X
for L being linear-transformation of X,Y st L is bijective holds
L @* l = l * (L ")
let l be Linear_Combination of X; :: thesis: for L being linear-transformation of X,Y st L is bijective holds
L @* l = l * (L ")
let L be linear-transformation of X,Y; :: thesis: ( L is bijective implies L @* l = l * (L ") )
assume A1: L is bijective ; :: thesis: L @* l = l * (L ")
then Q4: rng L = the carrier of Y by FUNCT_2:def 3;
then reconsider K = L " as Function of Y,X by A1, FUNCT_2:25;
P3: dom (l * K) = the carrier of Y by FUNCT_2:def 1;
X1: L | (Carrier l) is one-to-one by A1, FUNCT_1:52;
then P4: L .: (Carrier l) = Carrier (L @* l) by ZMODUL05:56;
for a being Element of Y holds (L @* l) . a = (l * K) . a

proof

let a be Element of Y; :: thesis: (L @* l) . a = (l * K) . a

per cases ( not a in Carrier (L @* l) or a in Carrier (L @* l) ) ;

suppose X0: not a in Carrier (L @* l) ; :: thesis: (L @* l) . a = (l * K) . a

reconsider v = K . a as Element of X ;
X4: L . v = a by Q4, A1, FUNCT_1:35;
Y2: not v in Carrier l by X0, X4, FUNCT_2:35, P4;
(l * K) . a = l . v by P3, FUNCT_1:12
.= 0. R by Y2 ;
hence (L @* l) . a = (l * K) . a by X0; :: thesis: verum

end;

suppose a in Carrier (L @* l) ; :: thesis: (L @* l) . a = (l * K) . a

then consider v being object such that
X5: ( v in dom L & v in Carrier l & a = L . v ) by FUNCT_1:def 6, P4;
reconsider v = v as Element of X by X5;
X6: K . a = v by A1, FUNCT_1:34, X5;
thus (L @* l) . a = l . v by ZMODUL05:54, X1, X5
.= (l * K) . a by P3, FUNCT_1:12, X6 ; :: thesis: verum

end;

end;

end;

hence L @* l = l * (L ") by FUNCT_2:def 8; :: thesis: verum