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 & the multF of G is having_a_unity & the multF of G is associative ) by GROUP_1:31, GROUP_1:34, GROUP_3:2;
assume A2: ( len F = len F1 & 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 A3: 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

let k be Element of NAT ; :: thesis: ( k in dom F implies F . k = the multF of G . (F1 . k),(F2 . k) )
assume A4: k in dom F ; :: thesis: F . k = the multF of G . (F1 . k),(F2 . k)
A5: ( dom F = Seg (len F) & dom F1 = Seg (len F1) & dom F2 = Seg (len F2) ) by FINSEQ_1:def 3;
thus F . k = (F1 /. k) * (F2 /. k) by A3, A4
.= the multF of G . (F1 . k),(F2 /. k) by A2, A4, A5, PARTFUN1:def 8
.= the multF of G . (F1 . k),(F2 . k) by A2, A4, A5, PARTFUN1:def 8 ; :: thesis: verum

end;

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