let G be Group; 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; ( 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
; ( 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
; ( 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)
; Product F = (Product F1) * (Product F2)
now 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;
( 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
;
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
;
verum end;
hence
Product F = (Product F1) * (Product F2)
by A1, A2, A3, FINSOP_1:9; verum