let R be Ring; :: thesis: for V, W being LeftMod of R
for l being Linear_Combination of V
for T being linear-transformation of V,W
for G being FinSequence of V st rng G = Carrier l & T | (Carrier l) is one-to-one holds
T * (l (#) G) = (T @* l) (#) (T * G)
let V, W be LeftMod of R; :: thesis: for l being Linear_Combination of V
for T being linear-transformation of V,W
for G being FinSequence of V st rng G = Carrier l & T | (Carrier l) is one-to-one holds
T * (l (#) G) = (T @* l) (#) (T * G)
let l be Linear_Combination of V; :: thesis: for T being linear-transformation of V,W
for G being FinSequence of V st rng G = Carrier l & T | (Carrier l) is one-to-one holds
T * (l (#) G) = (T @* l) (#) (T * G)
let T be linear-transformation of V,W; :: thesis: for G being FinSequence of V st rng G = Carrier l & T | (Carrier l) is one-to-one holds
T * (l (#) G) = (T @* l) (#) (T * G)
let G be FinSequence of V; :: thesis: ( rng G = Carrier l & T | (Carrier l) is one-to-one implies T * (l (#) G) = (T @* l) (#) (T * G) )
assume that
A1: rng G = Carrier l and
A2: T | (Carrier l) is one-to-one ; :: thesis: T * (l (#) G) = (T @* l) (#) (T * G)
reconsider R = (T @* l) (#) (T * G) as FinSequence of W ;
reconsider L = T * (l (#) G) as FinSequence of W ;
A3: len R = len (T * G) by VECTSP_6:def 5
.= len G by FINSEQ_2:33 ;
A4: len L = len (l (#) G) by FINSEQ_2:33
.= len G by VECTSP_6:def 5 ;
for k being Nat st 1 <= k & k <= len L holds
L . k = R . k

proof

A5: dom R = Seg (len G) by A3, FINSEQ_1:def 3;
let k be Nat; :: thesis: ( 1 <= k & k <= len L implies L . k = R . k )
assume A6: ( 1 <= k & k <= len L ) ; :: thesis: L . k = R . k
reconsider gk = G /. k as Element of V ;
len (l (#) G) = len G by VECTSP_6:def 5;
then A7: dom (l (#) G) = Seg (len G) by FINSEQ_1:def 3;
A8: k in dom (l (#) G) by A4, A6, A7;
then A9: k in dom G by A7, FINSEQ_1:def 3;
then A10: G . k = G /. k by PARTFUN1:def 6;
then reconsider Gk = G . k as Element of V ;
(T * G) . k = T . Gk by A9, FUNCT_1:13;
then reconsider TGk = (T * G) . k as Element of W ;
(l (#) G) . k = (l . gk) * gk by A8, VECTSP_6:def 5;
then A11: L . k = T . ((l . gk) * gk) by A8, FUNCT_1:13
.= (l . gk) * (T . gk) by MOD_2:def 2
.= (l . Gk) * TGk by A9, A10, FUNCT_1:13 ;
( G . k in rng G & (T * G) . k = T . (G . k) ) by A9, FUNCT_1:3, FUNCT_1:13;
then A12: (T @* l) . ((T * G) . k) = l . (G . k) by A1, A2, Th37;
dom T = [#] V by RANKNULL:7;
then dom (T * G) = dom G by A1, RELAT_1:27;
then (T * G) /. k = (T * G) . k by A9, PARTFUN1:def 6;
hence L . k = R . k by A5, A7, A8, A11, A12, VECTSP_6:def 5; :: thesis: verum

end;

hence T * (l (#) G) = (T @* l) (#) (T * G) by A3, A4; :: thesis: verum