let D be non empty set ; 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; 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; ( 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 )
; 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 S1[ Nat] means ( $1 <> 0 & $1 <= len F implies f . $1 = G . (Seg $1) );
A10:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A11:
(
n <> 0 &
n <= len F implies
f . n = G . (Seg n) )
;
S1[n + 1]
assume that
n + 1
<> 0
and A12:
n + 1
<= len F
;
f . (n + 1) = G . (Seg (n + 1))
now f . (n + 1) = G . (Seg (n + 1))per cases
( n = 0 or n <> 0 )
;
suppose A14:
n <> 0
;
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;
verum end; end; end;
hence
f . (n + 1) = G . (Seg (n + 1))
;
verum
end;
A20:
S1[ 0 ]
;
for n being Nat holds S1[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; verum