let D be non empty set ; :: thesis: for F, G, H being FinSequence of D
for g being BinOp of D st g is associative & g is commutative & len F >= 1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = g . (F . k),(G . k) ) holds
g "**" H = g . (g "**" F),(g "**" G)
let F, G, H be FinSequence of D; :: thesis: for g being BinOp of D st g is associative & g is commutative & len F >= 1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = g . (F . k),(G . k) ) holds
g "**" H = g . (g "**" F),(g "**" G)
let g be BinOp of D; :: thesis: ( g is associative & g is commutative & len F >= 1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = g . (F . k),(G . k) ) implies g "**" H = g . (g "**" F),(g "**" G) )
assume that
A1: g is associative and
A2: g is commutative ; :: thesis: ( not len F >= 1 or not len F = len G or not len F = len H or ex k being Element of NAT st
( k in dom F & not H . k = g . (F . k),(G . k) ) or g "**" H = g . (g "**" F),(g "**" G) )
defpred S₁[ Element of NAT ] means for F, G, H being FinSequence of D st len F >= 1 & len F = $1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = g . (F . k),(G . k) ) holds
g "**" H = g . (g "**" F),(g "**" G);
A3: S₁[ 0 ] ;

A4: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

let F, G, H be FinSequence of D; :: thesis: ( len F >= 1 & len F = k + 1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = g . (F . k),(G . k) ) implies g "**" H = g . (g "**" F),(g "**" G) )
assume that
len F >= 1 and
A6: len F = k + 1 and
A7: len F = len G and
A8: len F = len H and
A9: for k being Element of NAT st k in dom F holds
H . k = g . (F . k),(G . k) ; :: thesis: g "**" H = g . (g "**" F),(g "**" G)
reconsider f = F | (Seg k), gg = G | (Seg k), h = H | (Seg k) as FinSequence of D by FINSEQ_1:23;
A10: ( len f = k & len gg = k & len h = k ) by A6, A7, A8, FINSEQ_3:59;

A11: now

let i be Element of NAT ; :: thesis: ( i in dom f implies h . i = g . (f . i),(gg . i) )
assume A12: i in dom f ; :: thesis: h . i = g . (f . i),(gg . i)
then ( i in Seg (len f) & i in Seg (len gg) & i in Seg (len h) ) by A10, FINSEQ_1:def 3;
then ( i in dom f & i in dom gg & i in dom h ) by FINSEQ_1:def 3;
then A13: ( F . i = f . i & G . i = gg . i & H . i = h . i ) by FUNCT_1:70;
k <= k + 1 by NAT_1:12;
then Seg (len f) c= Seg (len F) by A6, A10, FINSEQ_1:7;
then Seg (len f) c= dom F by FINSEQ_1:def 3;
then dom f c= dom F by FINSEQ_1:def 3;
hence h . i = g . (f . i),(gg . i) by A9, A12, A13; :: thesis: verum

end;

now

per cases ( len f >= 1 or len f = 0 ) by NAT_1:14;

suppose A14: len f >= 1 ; :: thesis: g "**" H = g . (g "**" F),(g "**" G)

then A15: g "**" h = g . (g "**" f),(g "**" gg) by A5, A10, A11;
k + 1 in Seg (k + 1) by FINSEQ_1:6;
then A16: ( k + 1 in dom F & k + 1 in dom G & k + 1 in dom H ) by A6, A7, A8, FINSEQ_1:def 3;
then ( F . (k + 1) in rng F & G . (k + 1) in rng G & H . (k + 1) in rng H & rng F c= D & rng G c= D & rng H c= D ) by FINSEQ_1:def 4, FUNCT_1:def 5;
then reconsider d = F . (k + 1), d1 = G . (k + 1), d2 = H . (k + 1) as Element of D ;
A17: ( G = gg ^ <*d1*> & F = f ^ <*d*> & H = h ^ <*d2*> ) by A6, A7, A8, FINSEQ_3:61;
then A18: ( g "**" G = g . (g "**" gg),d1 & g "**" F = g . (g "**" f),d & g "**" <*d*> = d & g "**" <*d1*> = d1 ) by A10, A14, Lm4, Th5;
d2 = g . (F . (k + 1)),(G . (k + 1)) by A9, A16;
hence g "**" H = g . (g . (g "**" f),(g "**" gg)),(g . d,d1) by A10, A14, A15, A17, Th5
.= g . (g . (g . (g "**" f),(g "**" gg)),d),d1 by A1, BINOP_1:def 3
.= g . (g . (g "**" f),(g . (g "**" gg),d)),d1 by A1, BINOP_1:def 3
.= g . (g . (g "**" f),(g . d,(g "**" gg))),d1 by A2, BINOP_1:def 2
.= g . (g . (g "**" F),(g "**" gg)),d1 by A1, A18, BINOP_1:def 3
.= g . (g "**" F),(g "**" G) by A1, A18, BINOP_1:def 3 ;
:: thesis: verum

end;

suppose len f = 0 ; :: thesis: g "**" H = g . (g "**" F),(g "**" G)

then ( g "**" H = H . 1 & g "**" F = F . 1 & g "**" G = G . 1 & 1 in dom F ) by A6, A7, A8, A10, Lm11, FINSEQ_3:27;
hence g "**" H = g . (g "**" F),(g "**" G) by A9; :: thesis: verum

end;

end;

end;

hence g "**" H = g . (g "**" F),(g "**" G) ; :: thesis: verum

end;

end;

A19: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A3, A4);
assume ( len F >= 1 & len F = len G & len F = len H ) ; :: thesis: ( ex k being Element of NAT st
( k in dom F & not H . k = g . (F . k),(G . k) ) or g "**" H = g . (g "**" F),(g "**" G) )
hence ( ex k being Element of NAT st
( k in dom F & not H . k = g . (F . k),(G . k) ) or g "**" H = g . (g "**" F),(g "**" G) ) by A19; :: thesis: verum