let V be RealLinearSpace; :: thesis: for F, G being FinSequence of the carrier of V
for f being Function of the carrier of V,REAL holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
let F, G be FinSequence of the carrier of V; :: thesis: for f being Function of the carrier of V,REAL holds f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
let f be Function of the carrier of V,REAL ; :: thesis: f (#) (F ^ G) = (f (#) F) ^ (f (#) G)
set H = (f (#) F) ^ (f (#) G);
set I = F ^ G;
A1: len ((f (#) F) ^ (f (#) G)) = (len (f (#) F)) + (len (f (#) G)) by FINSEQ_1:35
.= (len F) + (len (f (#) G)) by RLVECT_2:def 9
.= (len F) + (len G) by RLVECT_2:def 9
.= len (F ^ G) by FINSEQ_1:35 ;
A2: ( len F = len (f (#) F) & len G = len (f (#) G) ) by RLVECT_2:def 9;

now

let k be Element of NAT ; :: thesis: ( k in dom ((f (#) F) ^ (f (#) G)) implies ((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k) )
assume A3: k in dom ((f (#) F) ^ (f (#) G)) ; :: thesis: ((f (#) F) ^ (f (#) G)) . k = (f . ((F ^ G) /. k)) * ((F ^ G) /. k)

now

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

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

then A5: k in dom F by A2, FINSEQ_3:31;
then A6: k in dom (F ^ G) by FINSEQ_3:24;
A7: F /. k = F . k by A5, PARTFUN1:def 8
.= (F ^ G) . k by A5, FINSEQ_1:def 7
.= (F ^ G) /. k by A6, PARTFUN1:def 8 ;
thus ((f (#) F) ^ (f (#) G)) . k = (f (#) F) . k by A4, FINSEQ_1:def 7
.= (f . ((F ^ G) /. k)) * ((F ^ G) /. k) by A4, A7, RLVECT_2:def 9 ; :: thesis: verum

end;

suppose 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)

then consider n being Nat such that
A8: n in dom (f (#) G) and
A9: k = (len (f (#) F)) + n ;
A10: n in NAT by ORDINAL1:def 13;
A11: n in dom G by A2, A8, FINSEQ_3:31;
A12: k in dom (F ^ G) by A1, A3, FINSEQ_3:31;
A13: G /. n = G . n by A11, PARTFUN1:def 8
.= (F ^ G) . k by A2, A9, A11, FINSEQ_1:def 7
.= (F ^ G) /. k by A12, PARTFUN1:def 8 ;
thus ((f (#) F) ^ (f (#) G)) . k = (f (#) G) . n by A8, A9, FINSEQ_1:def 7
.= (f . ((F ^ G) /. k)) * ((F ^ G) /. k) by A8, A10, A13, RLVECT_2:def 9 ; :: 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 A1, RLVECT_2:def 9; :: thesis: verum