let G be Group; :: thesis: for F, F1, F2 being FinSequence of the carrier of G st G is commutative Group & len F = len F1 & len F = len F2 & ( for k being Nat st k in dom F holds
F . k = (F1 /. k) * (F2 /. k) ) holds
Product F = (Product F1) * (Product F2)
let F, F1, F2 be FinSequence of the carrier of G; :: thesis: ( G is commutative Group & len F = len F1 & len F = len F2 & ( for k being Nat st k in dom F holds
F . k = (F1 /. k) * (F2 /. k) ) implies Product F = (Product F1) * (Product F2) )
set g = the multF of G;
assume G is commutative Group ; :: thesis: ( not len F = len F1 or not len F = len F2 or ex k being Nat st
( k in dom F & not F . k = (F1 /. k) * (F2 /. k) ) or Product F = (Product F1) * (Product F2) )
then A1: the multF of G is commutative by GROUP_3:2;
assume that
A2: len F = len F1 and
A3: len F = len F2 ; :: thesis: ( ex k being Nat st
( k in dom F & not F . k = (F1 /. k) * (F2 /. k) ) or Product F = (Product F1) * (Product F2) )
assume A4: for k being Nat st k in dom F holds
F . k = (F1 /. k) * (F2 /. k) ; :: thesis: Product F = (Product F1) * (Product F2)

now :: thesis: for k being Nat st k in dom F holds
F . k = the multF of G . ((F1 . k),(F2 . k))

A5: dom F2 = Seg (len F2) by FINSEQ_1:def 3;
A6: dom F1 = Seg (len F1) by FINSEQ_1:def 3;
let k be Nat; :: thesis: ( k in dom F implies F . k = the multF of G . ((F1 . k),(F2 . k)) )
A7: dom F = Seg (len F) by FINSEQ_1:def 3;
assume A8: k in dom F ; :: thesis: F . k = the multF of G . ((F1 . k),(F2 . k))
hence F . k = (F1 /. k) * (F2 /. k) by A4
.= the multF of G . ((F1 . k),(F2 /. k)) by A2, A8, A7, A6, PARTFUN1:def 6
.= the multF of G . ((F1 . k),(F2 . k)) by A3, A8, A7, A5, PARTFUN1:def 6 ;
:: thesis: verum

end;

hence Product F = (Product F1) * (Product F2) by A1, A2, A3, FINSOP_1:9; :: thesis: verum