let D be non empty set ; :: thesis: for F being FinSequence of D
for g being BinOp of D st len F >= 1 & g is associative & g is commutative holds
g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F))
let F be FinSequence of D; :: thesis: for g being BinOp of D st len F >= 1 & g is associative & g is commutative holds
g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F))
let g be BinOp of D; :: thesis: ( len F >= 1 & g is associative & g is commutative implies g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) )
assume that
A1: len F >= 1 and
A2: ( g is associative & g is commutative ) ; :: thesis: g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F))
set A = findom F;
set h = (NAT --> (the_unity_wrt g)) +* F;
A3: dom F = Seg (len F) by FINSEQ_1:def 3;
then consider G being Function of (Fin NAT),D such that
A4: g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) = G . (findom F) and
for d being Element of D st d is_a_unity_wrt g holds
G . {} = d and
A5: for n being Element of NAT holds G . {n} = ((NAT --> (the_unity_wrt g)) +* F) . n and
A6: for B being Element of Fin NAT st B c= findom F & B <> {} holds
for n being Element of NAT st n in (findom F) \ B holds
G . (B \/ {n}) = g . ((G . B),(((NAT --> (the_unity_wrt g)) +* F) . n)) by A1, A2, SETWISEO:def 3;
consider f being sequence of D such that
A7: f . 1 = F . 1 and
A8: for n being Nat st 0 <> n & n < len F holds
f . (n + 1) = g . ((f . n),(F . (n + 1))) and
A9: g "**" F = f . (len F) by A1, Def1;
defpred S₁[ Nat] means ( $1 <> 0 & $1 <= len F implies f . $1 = G . (Seg $1) );
A10: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A11: ( n <> 0 & n <= len F implies f . n = G . (Seg n) ) ; :: thesis: S₁[n + 1]
assume that
n + 1 <> 0 and
A12: n + 1 <= len F ; :: thesis: f . (n + 1) = G . (Seg (n + 1))

now :: thesis: f . (n + 1) = G . (Seg (n + 1))

per cases ( n = 0 or n <> 0 ) ;

suppose A13: n = 0 ; :: thesis: f . (n + 1) = G . (Seg (n + 1))

1 in dom F by A1, A3, FINSEQ_1:1;
then ((NAT --> (the_unity_wrt g)) +* F) . 1 = F . 1 by FUNCT_4:13;
hence f . (n + 1) = G . (Seg (n + 1)) by A7, A5, A13, FINSEQ_1:2; :: thesis: verum

end;

suppose A14: n <> 0 ; :: thesis: f . (n + 1) = G . (Seg (n + 1))

reconsider B = Seg n as Element of Fin NAT by FINSUB_1:def 5;
n + 1 >= 1 by NAT_1:12;
then A15: n + 1 in dom F by A12, FINSEQ_3:25;
A16: n < len F by A12, NAT_1:13;
then A17: f . (n + 1) = g . ((f . n),(F . (n + 1))) by A8, A14;
not n + 1 in Seg n by FINSEQ_3:10;
then A18: n + 1 in (findom F) \ (Seg n) by A15, XBOOLE_0:def 5;
A19: Seg n c= findom F by A3, A16, FINSEQ_1:5;
G . (Seg (n + 1)) = G . ((Seg n) \/ {(n + 1)}) by FINSEQ_1:9
.= g . ((G . B),(((NAT --> (the_unity_wrt g)) +* F) . (n + 1))) by A6, A14, A19, A18 ;
hence f . (n + 1) = G . (Seg (n + 1)) by A11, A12, A14, A17, A15, FUNCT_4:13, NAT_1:13; :: thesis: verum

end;

end;

end;

hence f . (n + 1) = G . (Seg (n + 1)) ; :: thesis: verum

end;

A20: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A20, A10);
hence g "**" F = g $$ ((findom F),((NAT --> (the_unity_wrt g)) +* F)) by A1, A9, A3, A4; :: thesis: verum