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 Element of 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 Element of 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 Element of 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 Element of 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 Element of NAT st k in dom F holds
F . k = (F1 /. k) * (F2 /. k) ; :: thesis: Product F = (Product F1) * (Product F2)

now

A6: dom F2 = Seg (len F2) by FINSEQ_1:def 3;
A7: dom F1 = Seg (len F1) by FINSEQ_1:def 3;
let k be Element of NAT ; :: thesis: ( k in dom F implies F . k = the multF of G . (F1 . k),(F2 . k) )
A8: dom F = Seg (len F) by FINSEQ_1:def 3;
assume A9: 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, A9, A8, A7, PARTFUN1:def 8
.= the multF of G . (F1 . k),(F2 . k) by A3, A9, A8, A6, PARTFUN1:def 8 ;
:: thesis: verum

end;

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