let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for F, G being FinSequence of V
for f being Function of V,GF holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
let V be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for F, G being FinSequence of V
for f being Function of V,GF holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
let F, G be FinSequence of V; :: thesis: for f being Function of V,GF holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
let f be Function of V,GF; :: thesis: f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
set H = (f (#) F) ^ (f (#) G);
set I = F ^ G;
A1: len F = len (f (#) F) by Def5;
A2: len ((f (#) F) ^ (f (#) G)) = (len (f (#) F)) + (len (f (#) G)) by FINSEQ_1:22
.= (len F) + (len (f (#) G)) by Def5
.= (len F) + (len G) by Def5
.= len (F ^ G) by FINSEQ_1:22 ;
A3: len G = len (f (#) G) by Def5;

now :: thesis: for k being Nat st k in dom ((f (#) F) ^ (f (#) G)) holds
((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k)

let k be Nat; :: thesis: ( k in dom ((f (#) F) ^ (f (#) G)) implies ((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k) )
assume A4: k in dom ((f (#) F) ^ (f (#) G)) ; :: thesis: ((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k)

now :: thesis: ((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k)

per cases ( k in dom (f (#) F) or ex n being Nat st
( n in dom (f (#) G) & k = (len (f (#) F)) + n ) ) by A4, FINSEQ_1:25;

suppose A5: k in dom (f (#) F) ; :: thesis: ((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k)

then A6: k in dom F by A1, FINSEQ_3:29;
then A7: k in dom (F ^ G) by FINSEQ_3:22;
A8: F /. k = F . k by A6, PARTFUN1:def 6
.= (F ^ G) . k by A6, FINSEQ_1:def 7
.= (F ^ G) /. k by A7, PARTFUN1:def 6 ;
thus ((f (#) F) ^ (f (#) G)) . k = (f (#) F) . k by A5, FINSEQ_1:def 7
.= (f . ((F ^ G) /. k)) * ((F ^ G) /. k) by A5, A8, Def5 ; :: thesis: verum

end;

suppose A9: ex n being Nat st
( n in dom (f (#) G) & k = (len (f (#) F)) + n ) ; :: thesis: ((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k)

A10: k in dom (F ^ G) by A2, A4, FINSEQ_3:29;
consider n being Nat such that
A11: n in dom (f (#) G) and
A12: k = (len (f (#) F)) + n by A9;
A13: n in dom G by A3, A11, FINSEQ_3:29;
then A14: G /. n = G . n by PARTFUN1:def 6
.= (F ^ G) . k by A1, A12, A13, FINSEQ_1:def 7
.= (F ^ G) /. k by A10, PARTFUN1:def 6 ;
thus ((f (#) F) ^ (f (#) G)) . k = (f (#) G) . n by A11, A12, FINSEQ_1:def 7
.= (f . ((F ^ G) /. k)) * ((F ^ G) /. k) by A11, A14, Def5 ; :: thesis: verum

end;

end;

end;

hence ((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k) ; :: thesis: verum

end;

hence f (#) (F ^ G) = (f (#) F) ^ (f (#) G) by A2, Def5; :: thesis: verum