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 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 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 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 Nat st
( k in dom F & not H . k = g . ((F . k),(G . k)) ) or g "**" H = g . ((g "**" F),(g "**" G)) )
defpred S₁[ 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 n being Nat st n in dom F holds
H . n = g . ((F . n),(G . n)) ) holds
g "**" H = g . ((g "**" F),(g "**" G));

A3: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: 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 n being Nat st n in dom F holds
H . n = g . ((F . n),(G . n)) ) implies g "**" H = g . ((g "**" F),(g "**" G)) )
assume that
len F >= 1 and
A5: len F = k + 1 and
A6: len F = len G and
A7: len F = len H and
A8: for k being 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:18;
A9: len h = k by A5, A7, FINSEQ_3:53;
A10: len f = k by A5, FINSEQ_3:53;
A11: len gg = k by A5, A6, FINSEQ_3:53;

A12: now :: thesis: for i being Nat st i in dom f holds
h . i = g . ((f . i),(gg . i))

k <= k + 1 by NAT_1:12;
then Seg (len f) c= Seg (len F) by A5, A10, FINSEQ_1:5;
then Seg (len f) c= dom F by FINSEQ_1:def 3;
then A13: dom f c= dom F by FINSEQ_1:def 3;
let i be Nat; :: thesis: ( i in dom f implies h . i = g . ((f . i),(gg . i)) )
assume A14: i in dom f ; :: thesis: h . i = g . ((f . i),(gg . i))
then i in Seg (len gg) by A10, A11, FINSEQ_1:def 3;
then i in dom gg by FINSEQ_1:def 3;
then A15: G . i = gg . i by FUNCT_1:47;
i in Seg (len h) by A10, A9, A14, FINSEQ_1:def 3;
then i in dom h by FINSEQ_1:def 3;
then A16: H . i = h . i by FUNCT_1:47;
F . i = f . i by A14, FUNCT_1:47;
hence h . i = g . ((f . i),(gg . i)) by A8, A14, A15, A16, A13; :: thesis: verum

end;

now :: thesis: g "**" H = g . ((g "**" F),(g "**" G))

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

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

A18: rng H c= D by FINSEQ_1:def 4;
A19: ( rng F c= D & rng G c= D ) by FINSEQ_1:def 4;
A20: k + 1 in Seg (k + 1) by FINSEQ_1:4;
then k + 1 in dom G by A5, A6, FINSEQ_1:def 3;
then A21: G . (k + 1) in rng G by FUNCT_1:def 3;
k + 1 in dom H by A5, A7, A20, FINSEQ_1:def 3;
then A22: H . (k + 1) in rng H by FUNCT_1:def 3;
A23: k + 1 in dom F by A5, A20, FINSEQ_1:def 3;
then F . (k + 1) in rng F by FUNCT_1:def 3;
then reconsider d = F . (k + 1), d1 = G . (k + 1), d2 = H . (k + 1) as Element of D by A21, A22, A19, A18;
A24: d2 = g . ((F . (k + 1)),(G . (k + 1))) by A8, A23;
F = f ^ <*d*> by A5, FINSEQ_3:55;
then A25: g "**" F = g . ((g "**" f),d) by A17, Th4;
G = gg ^ <*d1*> by A5, A6, FINSEQ_3:55;
then A26: g "**" G = g . ((g "**" gg),d1) by A10, A11, A17, Th4;
A27: H = h ^ <*d2*> by A5, A7, FINSEQ_3:55;
g "**" h = g . ((g "**" f),(g "**" gg)) by A4, A10, A11, A9, A12, A17;
hence g "**" H = g . ((g . ((g "**" f),(g "**" gg))),(g . (d,d1))) by A10, A9, A17, A27, A24, Th4
.= 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, A25, BINOP_1:def 3
.= g . ((g "**" F),(g "**" G)) by A1, A26, BINOP_1:def 3 ;
:: thesis: verum

end;

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

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

end;

end;

end;

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

end;

end;

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