let D be non empty set ; :: thesis: for A, M being BinOp of D
for F being non-empty non empty FinSequence of D * st len F = 1 & M is commutative & M is associative & A is commutative & A is associative holds
M $$ (([#] (dom F)),(A "**" F)) = A $$ (([#] (dom (App F))),(M "**" (App F)))
let A, M be BinOp of D; :: thesis: for F being non-empty non empty FinSequence of D * st len F = 1 & M is commutative & M is associative & A is commutative & A is associative holds
M $$ (([#] (dom F)),(A "**" F)) = A $$ (([#] (dom (App F))),(M "**" (App F)))
let F be non-empty non empty FinSequence of D * ; :: thesis: ( len F = 1 & M is commutative & M is associative & A is commutative & A is associative implies M $$ (([#] (dom F)),(A "**" F)) = A $$ (([#] (dom (App F))),(M "**" (App F))) )
set F1 = F . 1;
assume that
A1: len F = 1 and
A2: ( M is commutative & M is associative & A is commutative & A is associative ) ; :: thesis: M $$ (([#] (dom F)),(A "**" F)) = A $$ (([#] (dom (App F))),(M "**" (App F)))
A3: F = <*(F . 1)*> by A1, FINSEQ_1:40;
then dom F = {1} by FINSEQ_1:38, FINSEQ_1:2;
then A4: ( [#] (dom F) = {.1.} & 1 is Element of dom F ) by TARSKI:def 1;
then M $$ (([#] (dom F)),(A "**" F)) = (A "**" F) . 1 by A2, SETWISEO:17;
then A5: M $$ (([#] (dom F)),(A "**" F)) = A "**" (F . 1) by A4, Def10;
set f = M "**" (App F);
set X = dom (App F);
A6: dom (App F) = doms F by Def9;
consider G being Function of (Fin (dom (App F))),D such that
A7: A $$ (([#] (dom (App F))),(M "**" (App F))) = G . ([#] (dom (App F))) and
for e being Element of D st e is_a_unity_wrt A holds
G . {} = e and
A8: for x being Element of dom (App F) holds G . {x} = (M "**" (App F)) . x and
A9: for B9 being Element of Fin (dom (App F)) st B9 c= [#] (dom (App F)) & B9 <> {} holds
for x being Element of dom (App F) st x in ([#] (dom (App F))) \ B9 holds
G . (B9 \/ {x}) = A . ((G . B9),((M "**" (App F)) . x)) by A2, SETWISEO:def 3;
A10: len (F . 1) >= 1 + 0 by A4, NAT_1:13;
then consider s being sequence of D such that
A11: s . 1 = (F . 1) . 1 and
A12: for n being Nat st 0 <> n & n < len (F . 1) holds
s . (n + 1) = A . ((s . n),((F . 1) . (n + 1))) and
A13: A "**" (F . 1) = s . (len (F . 1)) by FINSOP_1:1;
deffunc H₁( Nat) -> set = { <*i*> where i is Element of NAT : i in Seg $1 } ;
defpred S₁[ Nat] means ( $1 <= len (F . 1) implies for B9 being Element of Fin (dom (App F)) st B9 = H₁($1) holds
G . B9 = s . $1 );
A14: S₁[1]

proof

assume A15: 1 <= len (F . 1) ; :: thesis: for B9 being Element of Fin (dom (App F)) st B9 = H₁(1) holds
G . B9 = s . 1
let B9 be Element of Fin (dom (App F)); :: thesis: ( B9 = H₁(1) implies G . B9 = s . 1 )
assume A16: B9 = H₁(1) ; :: thesis: G . B9 = s . 1
A17: 1 in dom (F . 1) by A15, FINSEQ_3:25;
then ( (F . 1) . 1 in rng (F . 1) & rng (F . 1) c= D ) by FUNCT_1:def 3;
then reconsider F11 = (F . 1) . 1 as Element of D ;
A18: H₁(1) c= {<*1*>}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in H₁(1) or y in {<*1*>} )
assume y in H₁(1) ; :: thesis: y in {<*1*>}
then consider i being Element of NAT such that
A19: ( <*i*> = y & i in Seg 1 ) ;
i = 1 by A19, FINSEQ_1:2, TARSKI:def 1;
hence y in {<*1*>} by A19, TARSKI:def 1; :: thesis: verum

end;

{<*1*>} c= H₁(1)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in {<*1*>} or y in H₁(1) )
assume y in {<*1*>} ; :: thesis: y in H₁(1)
then ( y = <*1*> & 1 in Seg 1 ) by TARSKI:def 1;
hence y in H₁(1) ; :: thesis: verum

end;

then A20: H₁(1) = {<*1*>} by A18;
A21: ( <*1*> in B9 & B9 c= dom (App F) ) by A16, A20, TARSKI:def 1, FINSUB_1:def 5;
then G . B9 = (M "**" (App F)) . <*1*> by A16, A20, A8;
then G . B9 = M "**" ((App F) . <*1*>) by A21, Def10;
then G . B9 = M "**" <*F11*> by A3, Th60, A17;
hence G . B9 = s . 1 by A11, FINSOP_1:11; :: thesis: verum

end;

A22: for j being Nat st 1 <= j & S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( 1 <= j & S₁[j] implies S₁[j + 1] )
assume that
A23: 1 <= j and
A24: S₁[j] ; :: thesis: S₁[j + 1]
set j1 = j + 1;
assume A25: j + 1 <= len (F . 1) ; :: thesis: for B9 being Element of Fin (dom (App F)) st B9 = H₁(j + 1) holds
G . B9 = s . (j + 1)
j + 1 in dom (F . 1) by NAT_1:11, A25, FINSEQ_3:25;
then ( (F . 1) . (j + 1) in rng (F . 1) & rng (F . 1) c= D ) by FUNCT_1:def 3;
then reconsider F1j1 = (F . 1) . (j + 1) as Element of D ;
let B9 be Element of Fin (dom (App F)); :: thesis: ( B9 = H₁(j + 1) implies G . B9 = s . (j + 1) )
assume A26: B9 = H₁(j + 1) ; :: thesis: G . B9 = s . (j + 1)
A27: j < len (F . 1) by A25, NAT_1:13;
H₁(j) c= dom (App F)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in H₁(j) or y in dom (App F) )
assume y in H₁(j) ; :: thesis: y in dom (App F)
then consider i being Element of NAT such that
A28: ( <*i*> = y & i in Seg j ) ;
A29: ( 1 <= i & i <= j ) by A28, FINSEQ_1:1;
then i <= len (F . 1) by A27, XXREAL_0:2;
then ( <*i*> . 1 in dom (F . 1) & len <*i*> = 1 ) by FINSEQ_1:40, A29, FINSEQ_3:25;
hence y in dom (App F) by A28, A6, A3, Th51; :: thesis: verum

end;

then reconsider Rj = H₁(j) as Element of Fin (dom (App F)) by FINSUB_1:def 5;
A30: Rj c= B9

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Rj or y in B9 )
assume y in Rj ; :: thesis: y in B9
then consider i being Element of NAT such that
A31: ( <*i*> = y & i in Seg j ) ;
A32: ( 1 <= i & i <= j ) by A31, FINSEQ_1:1;
then i <= j + 1 by NAT_1:13;
then i in Seg (j + 1) by A32;
hence y in B9 by A31, A26; :: thesis: verum

end;

j + 1 in Seg (j + 1) by FINSEQ_1:4;
then <*(j + 1)*> in B9 by A26;
then A33: {<*(j + 1)*>} c= B9 by ZFMISC_1:31;
B9 c= Rj \/ {<*(j + 1)*>}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in B9 or y in Rj \/ {<*(j + 1)*>} )
assume y in B9 ; :: thesis: y in Rj \/ {<*(j + 1)*>}
then consider i being Element of NAT such that
A34: ( <*i*> = y & i in Seg (j + 1) ) by A26;
i in (Seg j) \/ {(j + 1)} by A34, FINSEQ_1:9;
then ( i in Seg j or i in {(j + 1)} ) by XBOOLE_0:def 3;
then ( i in Seg j or i = j + 1 ) by TARSKI:def 1;
then ( <*i*> in Rj or <*i*> in {<*(j + 1)*>} ) by TARSKI:def 1;
hence y in Rj \/ {<*(j + 1)*>} by A34, XBOOLE_0:def 3; :: thesis: verum

end;

then A35: B9 = Rj \/ {<*(j + 1)*>} by A33, A30, XBOOLE_1:8;
A36: G . Rj = s . j by A24, A25, NAT_1:13;
A37: Rj c= [#] (dom (App F)) by FINSUB_1:def 5;
j in Seg j by A23;
then A38: <*j*> in Rj ;
A39: ( <*(j + 1)*> . 1 in dom (F . 1) & len <*(j + 1)*> = 1 & <*(j + 1)*> . 1 = j + 1 ) by NAT_1:11, A25, FINSEQ_1:40, FINSEQ_3:25;
then reconsider J = <*(j + 1)*> as Element of dom (App F) by A6, A3, Th51;
(M "**" (App F)) . J = M "**" ((App F) . <*(j + 1)*>) by Def10;
then (M "**" (App F)) . J = M "**" <*F1j1*> by A3, A39, Th60;
then A40: (M "**" (App F)) . J = F1j1 by FINSOP_1:11;
not J in Rj

proof

assume J in Rj ; :: thesis: contradiction
then consider i being Element of NAT such that
A41: ( <*i*> = J & i in Seg j ) ;
( i <= j & j + 1 = i ) by FINSEQ_1:76, A41, FINSEQ_1:1;
hence contradiction by NAT_1:13; :: thesis: verum

end;

then J in ([#] (dom (App F))) \ Rj by XBOOLE_0:def 5;
then G . B9 = A . ((s . j),F1j1) by A40, A36, A35, A37, A38, A9;
hence G . B9 = s . (j + 1) by A12, A25, NAT_1:13, A23; :: thesis: verum

end;

A42: for i being Nat st 1 <= i holds
S₁[i] from NAT_1:sch 8(A14, A22);
H₁( len (F . 1)) = dom (App F)

proof

thus H₁( len (F . 1)) c= dom (App F) :: according to XBOOLE_0:def 10 :: thesis: dom (App F) c= H₁( len (F . 1))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in H₁( len (F . 1)) or y in dom (App F) )
assume y in H₁( len (F . 1)) ; :: thesis: y in dom (App F)
then consider i being Element of NAT such that
A43: ( <*i*> = y & i in Seg (len (F . 1)) ) ;
( <*i*> . 1 in dom (F . 1) & len <*i*> = 1 ) by FINSEQ_1:40, A43, FINSEQ_1:def 3;
hence y in dom (App F) by A43, A6, A3, Th51; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in dom (App F) or y in H₁( len (F . 1)) )
assume A44: y in dom (App F) ; :: thesis: y in H₁( len (F . 1))
reconsider f = y as FinSequence by A44;
( len f = 1 & f . 1 in dom (F . 1) ) by Th51, A44, A3;
then ( f = <*(f . 1)*> & f . 1 in Seg (len (F . 1)) ) by FINSEQ_1:40, FINSEQ_1:def 3;
hence y in H₁( len (F . 1)) ; :: thesis: verum

end;

hence M $$ (([#] (dom F)),(A "**" F)) = A $$ (([#] (dom (App F))),(M "**" (App F))) by A5, A13, A7, A42, A10; :: thesis: verum