let D be non empty set ; :: thesis: for A being BinOp of D
for d1, d2 being Element of D
for f being FinSequence of D st A is having_a_unity & A is associative & A is commutative & A is having_an_inverseOp holds
for F being non empty finite set st union F c= dom f holds
for F1, F2 being finite set st F1 = UNION (F,(bool {((len f) + 1)})) & F2 = UNION (F,(bool {((len f) + 1),((len f) + 2)})) holds
ex E1 being Enumeration of F1 ex E2 being Enumeration of F2 st A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,F2)) * E2) = (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F1)) * E1)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>),A,F1)) * E1))
let A be BinOp of D; :: thesis: for d1, d2 being Element of D
for f being FinSequence of D st A is having_a_unity & A is associative & A is commutative & A is having_an_inverseOp holds
for F being non empty finite set st union F c= dom f holds
for F1, F2 being finite set st F1 = UNION (F,(bool {((len f) + 1)})) & F2 = UNION (F,(bool {((len f) + 1),((len f) + 2)})) holds
ex E1 being Enumeration of F1 ex E2 being Enumeration of F2 st A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,F2)) * E2) = (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F1)) * E1)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>),A,F1)) * E1))
let d1, d2 be Element of D; :: thesis: for f being FinSequence of D st A is having_a_unity & A is associative & A is commutative & A is having_an_inverseOp holds
for F being non empty finite set st union F c= dom f holds
for F1, F2 being finite set st F1 = UNION (F,(bool {((len f) + 1)})) & F2 = UNION (F,(bool {((len f) + 1),((len f) + 2)})) holds
ex E1 being Enumeration of F1 ex E2 being Enumeration of F2 st A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,F2)) * E2) = (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F1)) * E1)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>),A,F1)) * E1))
let f be FinSequence of D; :: thesis: ( A is having_a_unity & A is associative & A is commutative & A is having_an_inverseOp implies for F being non empty finite set st union F c= dom f holds
for F1, F2 being finite set st F1 = UNION (F,(bool {((len f) + 1)})) & F2 = UNION (F,(bool {((len f) + 1),((len f) + 2)})) holds
ex E1 being Enumeration of F1 ex E2 being Enumeration of F2 st A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,F2)) * E2) = (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F1)) * E1)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>),A,F1)) * E1)) )
assume A1: ( A is having_a_unity & A is associative & A is commutative & A is having_an_inverseOp ) ; :: thesis: for F being non empty finite set st union F c= dom f holds
for F1, F2 being finite set st F1 = UNION (F,(bool {((len f) + 1)})) & F2 = UNION (F,(bool {((len f) + 1),((len f) + 2)})) holds
ex E1 being Enumeration of F1 ex E2 being Enumeration of F2 st A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,F2)) * E2) = (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F1)) * E1)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>),A,F1)) * E1))
let F be non empty finite set ; :: thesis: ( union F c= dom f implies for F1, F2 being finite set st F1 = UNION (F,(bool {((len f) + 1)})) & F2 = UNION (F,(bool {((len f) + 1),((len f) + 2)})) holds
ex E1 being Enumeration of F1 ex E2 being Enumeration of F2 st A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,F2)) * E2) = (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F1)) * E1)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>),A,F1)) * E1)) )
assume A2: union F c= dom f ; :: thesis: for F1, F2 being finite set st F1 = UNION (F,(bool {((len f) + 1)})) & F2 = UNION (F,(bool {((len f) + 1),((len f) + 2)})) holds
ex E1 being Enumeration of F1 ex E2 being Enumeration of F2 st A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,F2)) * E2) = (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F1)) * E1)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>),A,F1)) * E1))
let F1, F2 be finite set ; :: thesis: ( F1 = UNION (F,(bool {((len f) + 1)})) & F2 = UNION (F,(bool {((len f) + 1),((len f) + 2)})) implies ex E1 being Enumeration of F1 ex E2 being Enumeration of F2 st A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,F2)) * E2) = (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F1)) * E1)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>),A,F1)) * E1)) )
assume A3: ( F1 = UNION (F,(bool {((len f) + 1)})) & F2 = UNION (F,(bool {((len f) + 1),((len f) + 2)})) ) ; :: thesis: ex E1 being Enumeration of F1 ex E2 being Enumeration of F2 st A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,F2)) * E2) = (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F1)) * E1)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>),A,F1)) * E1))
set L = len f;
set U1 = UNION (F,{{((len f) + 1)}});
set U2 = UNION (F,{{((len f) + 2)}});
set U12 = UNION (F,{{((len f) + 1),((len f) + 2)}});
set E = the Enumeration of F;
set I = the_inverseOp_wrt A;
set f12 = (f ^ <*d1*>) ^ <*d2*>;
set fA = f ^ <*(A . (d1,d2))*>;
set fAI = f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>;
A4: ( 0 + (len f) < 2 + (len f) & 1 + (len f) < 2 + (len f) ) by XREAL_1:8;
then A5: not (len f) + 2 in union F by A2, FINSEQ_3:25;
A6: len f < (len f) + 1 by NAT_1:13;
then A7: not (len f) + 1 in union F by A2, FINSEQ_3:25;
then consider E1 being Enumeration of UNION (F,{{((len f) + 1)}}) such that
A8: for i being Nat st i in dom the Enumeration of F holds
E1 . i = {((len f) + 1)} \/ ( the Enumeration of F . i) by Th88, ZFMISC_1:50;
(len f) + 1 in {((len f) + 1)} by TARSKI:def 1;
then A9: ( (len f) + 1 in {((len f) + 1)} \/ (meet F) & {((len f) + 1)} \/ (meet F) = meet (UNION (F,{{((len f) + 1)}})) ) by XBOOLE_0:def 3, SETFAM_1:24;
A10: not (len f) + 2 in union (UNION (F,{{((len f) + 1)}}))

proof

assume (len f) + 2 in union (UNION (F,{{((len f) + 1)}})) ; :: thesis: contradiction
then consider XY being set such that
A11: ( (len f) + 2 in XY & XY in UNION (F,{{((len f) + 1)}}) ) by TARSKI:def 4;
consider X, Y being set such that
A12: ( X in F & Y in {{((len f) + 1)}} & XY = X \/ Y ) by A11, SETFAM_1:def 4;
(len f) + 1 <> (len f) + 2 ;
then ( not (len f) + 2 in {((len f) + 1)} & {((len f) + 1)} = Y ) by A12, TARSKI:def 1;
then ( (len f) + 2 in X & X c= union F ) by A11, A12, XBOOLE_0:def 3, ZFMISC_1:74;
then (len f) + 2 in dom f by A2;
hence contradiction by A4, FINSEQ_3:25; :: thesis: verum

end;

(len f) + 2 in {((len f) + 2)} by TARSKI:def 1;
then A13: ( (len f) + 2 in {((len f) + 2)} \/ (meet F) & {((len f) + 2)} \/ (meet F) = meet (UNION (F,{{((len f) + 2)}})) ) by XBOOLE_0:def 3, SETFAM_1:24;
A14: not (len f) + 1 in union (UNION (F,{{((len f) + 2)}}))

proof

assume (len f) + 1 in union (UNION (F,{{((len f) + 2)}})) ; :: thesis: contradiction
then consider XY being set such that
A15: ( (len f) + 1 in XY & XY in UNION (F,{{((len f) + 2)}}) ) by TARSKI:def 4;
consider X, Y being set such that
A16: ( X in F & Y in {{((len f) + 2)}} & XY = X \/ Y ) by A15, SETFAM_1:def 4;
(len f) + 1 <> (len f) + 2 ;
then ( not (len f) + 1 in {((len f) + 2)} & {((len f) + 2)} = Y ) by A16, TARSKI:def 1;
then ( (len f) + 1 in X & X c= union F ) by A15, A16, XBOOLE_0:def 3, ZFMISC_1:74;
then (len f) + 1 in dom f by A2;
hence contradiction by A6, FINSEQ_3:25; :: thesis: verum

end;

for a being set st a in UNION (F,{{((len f) + 1),((len f) + 2)}}) holds
( (len f) + 1 in a & (len f) + 2 in a )

proof

let a be set ; :: thesis: ( a in UNION (F,{{((len f) + 1),((len f) + 2)}}) implies ( (len f) + 1 in a & (len f) + 2 in a ) )
assume a in UNION (F,{{((len f) + 1),((len f) + 2)}}) ; :: thesis: ( (len f) + 1 in a & (len f) + 2 in a )
then consider X, Y being set such that
A17: ( X in F & Y in {{((len f) + 1),((len f) + 2)}} & a = X \/ Y ) by SETFAM_1:def 4;
( (len f) + 1 in {((len f) + 1),((len f) + 2)} & (len f) + 2 in {((len f) + 1),((len f) + 2)} & {((len f) + 1),((len f) + 2)} = Y ) by TARSKI:def 1, TARSKI:def 2, A17;
hence ( (len f) + 1 in a & (len f) + 2 in a ) by A17, XBOOLE_0:def 3; :: thesis: verum

end;

then for a being set holds
( ( a in UNION (F,{{((len f) + 1),((len f) + 2)}}) implies (len f) + 1 in a ) & ( a in UNION (F,{{((len f) + 1),((len f) + 2)}}) implies (len f) + 2 in a ) ) ;
then A18: ( (len f) + 1 in meet (UNION (F,{{((len f) + 1),((len f) + 2)}})) & (len f) + 2 in meet (UNION (F,{{((len f) + 1),((len f) + 2)}})) ) by SETFAM_1:def 1;
consider E2 being Enumeration of UNION (F,{{((len f) + 2)}}) such that
A19: for i being Nat st i in dom the Enumeration of F holds
E2 . i = {((len f) + 2)} \/ ( the Enumeration of F . i) by Th88, A5, ZFMISC_1:50;
consider E12 being Enumeration of UNION (F,{{((len f) + 1),((len f) + 2)}}) such that
A20: for i being Nat st i in dom the Enumeration of F holds
E12 . i = {((len f) + 1),((len f) + 2)} \/ ( the Enumeration of F . i) by Th88, A5, A7, ZFMISC_1:51;
F misses UNION (F,{{((len f) + 1)}})

proof

assume F meets UNION (F,{{((len f) + 1)}}) ; :: thesis: contradiction
then consider x being object such that
A21: ( x in F & x in UNION (F,{{((len f) + 1)}}) ) by XBOOLE_0:3;
consider X, Y being set such that
A22: ( X in F & Y in {{((len f) + 1)}} & x = X \/ Y ) by A21, SETFAM_1:def 4;
Y = {((len f) + 1)} by A22, TARSKI:def 1;
then (len f) + 1 in Y by TARSKI:def 1;
then (len f) + 1 in X \/ Y by XBOOLE_0:def 3;
hence contradiction by A7, A21, A22, TARSKI:def 4; :: thesis: verum

end;

then reconsider EE1 = the Enumeration of F ^ E1 as Enumeration of F \/ (UNION (F,{{((len f) + 1)}})) by Th79;
UNION (F,{{((len f) + 1)}}) misses UNION (F,{{((len f) + 2)}})

proof

assume UNION (F,{{((len f) + 1)}}) meets UNION (F,{{((len f) + 2)}}) ; :: thesis: contradiction
then consider x being object such that
A23: ( x in UNION (F,{{((len f) + 1)}}) & x in UNION (F,{{((len f) + 2)}}) ) by XBOOLE_0:3;
consider X1, Y1 being set such that
A24: ( X1 in F & Y1 in {{((len f) + 1)}} & x = X1 \/ Y1 ) by A23, SETFAM_1:def 4;
Y1 = {((len f) + 1)} by A24, TARSKI:def 1;
then (len f) + 1 in Y1 by TARSKI:def 1;
then (len f) + 1 in X1 \/ Y1 by XBOOLE_0:def 3;
hence contradiction by A14, A23, A24, TARSKI:def 4; :: thesis: verum

end;

then reconsider E2E1 = E2 ^ E1 as Enumeration of (UNION (F,{{((len f) + 2)}})) \/ (UNION (F,{{((len f) + 1)}})) by Th79;
F misses UNION (F,{{((len f) + 1),((len f) + 2)}})

proof

assume F meets UNION (F,{{((len f) + 1),((len f) + 2)}}) ; :: thesis: contradiction
then consider x being object such that
A25: ( x in F & x in UNION (F,{{((len f) + 1),((len f) + 2)}}) ) by XBOOLE_0:3;
consider X, Y being set such that
A26: ( X in F & Y in {{((len f) + 1),((len f) + 2)}} & x = X \/ Y ) by A25, SETFAM_1:def 4;
Y = {((len f) + 1),((len f) + 2)} by A26, TARSKI:def 1;
then (len f) + 1 in Y by TARSKI:def 2;
then (len f) + 1 in X \/ Y by XBOOLE_0:def 3;
hence contradiction by A7, A25, A26, TARSKI:def 4; :: thesis: verum

end;

then reconsider EE12 = the Enumeration of F ^ E12 as Enumeration of F \/ (UNION (F,{{((len f) + 1),((len f) + 2)}})) by Th79;
A27: ( card (UNION (F,{{((len f) + 1),((len f) + 2)}})) = card F & card F = card (UNION (F,{{((len f) + 2)}})) ) by A5, A7, ZFMISC_1:51, Th8, ZFMISC_1:50;
A28: ( card (UNION (F,{{((len f) + 1),((len f) + 2)}})) = card F & card F = card (UNION (F,{{((len f) + 1)}})) ) by A5, A7, ZFMISC_1:51, Th8, ZFMISC_1:50;
( len E1 = card (UNION (F,{{((len f) + 1)}})) & len E12 = card (UNION (F,{{((len f) + 1),((len f) + 2)}})) & len the Enumeration of F = card F ) by CARD_1:def 7;
then A29: ( dom E1 = dom the Enumeration of F & dom the Enumeration of F = dom E12 ) by A28, FINSEQ_3:30;
A30: len (f ^ <*(A . (d1,d2))*>) = (len f) + 1 by FINSEQ_2:16;
then A31: dom (f ^ <*(A . (d1,d2))*>) = Seg ((len f) + 1) by FINSEQ_1:def 3;
len (f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>) = (len f) + 1 by FINSEQ_2:16;
then A32: dom (f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>) = dom (f ^ <*(A . (d1,d2))*>) by A31, FINSEQ_1:def 3;
not (len f) + 2 in dom (f ^ <*(A . (d1,d2))*>) by A30, A4, FINSEQ_3:25;
then A33: {((len f) + 2)} misses dom (f ^ <*(A . (d1,d2))*>) by ZFMISC_1:50;
A34: for i being Nat st i in dom E1 holds
(dom (f ^ <*(A . (d1,d2))*>)) /\ (E1 . i) = (dom (f ^ <*(A . (d1,d2))*>)) /\ (E12 . i)

proof

let i be Nat; :: thesis: ( i in dom E1 implies (dom (f ^ <*(A . (d1,d2))*>)) /\ (E1 . i) = (dom (f ^ <*(A . (d1,d2))*>)) /\ (E12 . i) )
assume A35: i in dom E1 ; :: thesis: (dom (f ^ <*(A . (d1,d2))*>)) /\ (E1 . i) = (dom (f ^ <*(A . (d1,d2))*>)) /\ (E12 . i)
A36: E12 . i = {((len f) + 1),((len f) + 2)} \/ ( the Enumeration of F . i) by A35, A20, A29;
A37: E1 . i = {((len f) + 1)} \/ ( the Enumeration of F . i) by A35, A8, A29;
{((len f) + 1),((len f) + 2)} = {((len f) + 1)} \/ {((len f) + 2)} by ENUMSET1:1;
then E12 . i = (E1 . i) \/ {((len f) + 2)} by A36, A37, XBOOLE_1:4;
then (dom (f ^ <*(A . (d1,d2))*>)) /\ (E12 . i) = ((dom (f ^ <*(A . (d1,d2))*>)) /\ (E1 . i)) \/ ((dom (f ^ <*(A . (d1,d2))*>)) /\ {((len f) + 2)}) by XBOOLE_1:23;
hence (dom (f ^ <*(A . (d1,d2))*>)) /\ (E1 . i) = (dom (f ^ <*(A . (d1,d2))*>)) /\ (E12 . i) by A33; :: thesis: verum

end;

A38: for i being Nat st i in dom the Enumeration of F holds
(dom (f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>)) /\ ( the Enumeration of F . i) = (dom (f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>)) /\ (E2 . i)

proof

let i be Nat; :: thesis: ( i in dom the Enumeration of F implies (dom (f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>)) /\ ( the Enumeration of F . i) = (dom (f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>)) /\ (E2 . i) )
assume A39: i in dom the Enumeration of F ; :: thesis: (dom (f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>)) /\ ( the Enumeration of F . i) = (dom (f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>)) /\ (E2 . i)
E2 . i = {((len f) + 2)} \/ ( the Enumeration of F . i) by A39, A19;
then (dom (f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>)) /\ (E2 . i) = ((dom (f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>)) /\ ( the Enumeration of F . i)) \/ ((dom (f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>)) /\ {((len f) + 2)}) by XBOOLE_1:23;
hence (dom (f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>)) /\ ( the Enumeration of F . i) = (dom (f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>)) /\ (E2 . i) by A33, A32; :: thesis: verum

end;

F \/ (UNION (F,{{((len f) + 1),((len f) + 2)}})) misses (UNION (F,{{((len f) + 2)}})) \/ (UNION (F,{{((len f) + 1)}}))

proof

assume F \/ (UNION (F,{{((len f) + 1),((len f) + 2)}})) meets (UNION (F,{{((len f) + 2)}})) \/ (UNION (F,{{((len f) + 1)}})) ; :: thesis: contradiction
then consider x being object such that
A40: ( x in F \/ (UNION (F,{{((len f) + 1),((len f) + 2)}})) & x in (UNION (F,{{((len f) + 2)}})) \/ (UNION (F,{{((len f) + 1)}})) ) by XBOOLE_0:3;

per cases ( x in F or x in UNION (F,{{((len f) + 1),((len f) + 2)}}) ) by A40, XBOOLE_0:def 3;

suppose A41: x in F ; :: thesis: contradiction

per cases ( x in UNION (F,{{((len f) + 2)}}) or x in UNION (F,{{((len f) + 1)}}) ) by A40, XBOOLE_0:def 3;

suppose x in UNION (F,{{((len f) + 2)}}) ; :: thesis: contradiction

then consider X, Y being set such that
A42: ( X in F & Y in {{((len f) + 2)}} & x = X \/ Y ) by SETFAM_1:def 4;
Y = {((len f) + 2)} by A42, TARSKI:def 1;
then (len f) + 2 in Y by TARSKI:def 1;
then (len f) + 2 in X \/ Y by XBOOLE_0:def 3;
hence contradiction by A5, A42, A41, TARSKI:def 4; :: thesis: verum

end;

suppose x in UNION (F,{{((len f) + 1)}}) ; :: thesis: contradiction

then consider X, Y being set such that
A43: ( X in F & Y in {{((len f) + 1)}} & x = X \/ Y ) by SETFAM_1:def 4;
Y = {((len f) + 1)} by A43, TARSKI:def 1;
then (len f) + 1 in Y by TARSKI:def 1;
then (len f) + 1 in X \/ Y by XBOOLE_0:def 3;
hence contradiction by A7, A43, A41, TARSKI:def 4; :: thesis: verum

end;

end;

end;

suppose x in UNION (F,{{((len f) + 1),((len f) + 2)}}) ; :: thesis: contradiction

then consider X, Y being set such that
A44: ( X in F & Y in {{((len f) + 1),((len f) + 2)}} & x = X \/ Y ) by SETFAM_1:def 4;
A45: ( x in UNION (F,{{((len f) + 1)}}) or x in UNION (F,{{((len f) + 2)}}) ) by A40, XBOOLE_0:def 3;
Y = {((len f) + 1),((len f) + 2)} by A44, TARSKI:def 1;
then ( (len f) + 1 in Y & (len f) + 2 in Y ) by TARSKI:def 2;
then ( (len f) + 1 in X \/ Y & (len f) + 2 in X \/ Y ) by XBOOLE_0:def 3;
hence contradiction by A14, A10, A45, A44, TARSKI:def 4; :: thesis: verum

end;

end;

end;

then reconsider ET = EE12 ^ E2E1 as Enumeration of (F \/ (UNION (F,{{((len f) + 1),((len f) + 2)}}))) \/ ((UNION (F,{{((len f) + 2)}})) \/ (UNION (F,{{((len f) + 1)}}))) by Th79;
A46: ({{}} \/ {{((len f) + 1),((len f) + 2)}}) \/ ({{((len f) + 1)}} \/ {{((len f) + 2)}}) = bool {((len f) + 1),((len f) + 2)}

proof

thus ({{}} \/ {{((len f) + 1),((len f) + 2)}}) \/ ({{((len f) + 1)}} \/ {{((len f) + 2)}}) c= bool {((len f) + 1),((len f) + 2)} :: according to XBOOLE_0:def 10 :: thesis: bool {((len f) + 1),((len f) + 2)} c= ({{}} \/ {{((len f) + 1),((len f) + 2)}}) \/ ({{((len f) + 1)}} \/ {{((len f) + 2)}})

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in ({{}} \/ {{((len f) + 1),((len f) + 2)}}) \/ ({{((len f) + 1)}} \/ {{((len f) + 2)}}) or y in bool {((len f) + 1),((len f) + 2)} )
reconsider a = y as set by TARSKI:1;
assume y in ({{}} \/ {{((len f) + 1),((len f) + 2)}}) \/ ({{((len f) + 1)}} \/ {{((len f) + 2)}}) ; :: thesis: y in bool {((len f) + 1),((len f) + 2)}
then ( y in {{}} \/ {{((len f) + 1),((len f) + 2)}} or y in {{((len f) + 1)}} \/ {{((len f) + 2)}} ) by XBOOLE_0:def 3;
then ( y in {{}} or y in {{((len f) + 1),((len f) + 2)}} or y in {{((len f) + 1)}} or y in {{((len f) + 2)}} ) by XBOOLE_0:def 3;
then ( y = {} or y = {((len f) + 1),((len f) + 2)} or y = {((len f) + 1)} or y = {((len f) + 2)} ) by TARSKI:def 1;
then a c= {((len f) + 1),((len f) + 2)} by ZFMISC_1:36;
hence y in bool {((len f) + 1),((len f) + 2)} ; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in bool {((len f) + 1),((len f) + 2)} or y in ({{}} \/ {{((len f) + 1),((len f) + 2)}}) \/ ({{((len f) + 1)}} \/ {{((len f) + 2)}}) )
assume A47: y in bool {((len f) + 1),((len f) + 2)} ; :: thesis: y in ({{}} \/ {{((len f) + 1),((len f) + 2)}}) \/ ({{((len f) + 1)}} \/ {{((len f) + 2)}})
reconsider y = y as set by TARSKI:1;
( y = {} or y = {((len f) + 1),((len f) + 2)} or y = {((len f) + 1)} or y = {((len f) + 2)} ) by A47, ZFMISC_1:36;
then ( y in {{}} or y in {{((len f) + 1),((len f) + 2)}} or y in {{((len f) + 1)}} or y in {{((len f) + 2)}} ) by TARSKI:def 1;
then ( y in {{}} \/ {{((len f) + 1),((len f) + 2)}} or y in {{((len f) + 1)}} \/ {{((len f) + 2)}} ) by XBOOLE_0:def 3;
hence y in ({{}} \/ {{((len f) + 1),((len f) + 2)}}) \/ ({{((len f) + 1)}} \/ {{((len f) + 2)}}) by XBOOLE_0:def 3; :: thesis: verum

end;

A48: F = UNION (F,{{}})

proof

thus F c= UNION (F,{{}}) :: according to XBOOLE_0:def 10 :: thesis: UNION (F,{{}}) c= F

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in F or y in UNION (F,{{}}) )
assume A49: y in F ; :: thesis: y in UNION (F,{{}})
reconsider y = y as set by TARSKI:1;
{} in {{}} by TARSKI:def 1;
then y \/ {} in UNION (F,{{}}) by A49, SETFAM_1:def 4;
hence y in UNION (F,{{}}) ; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in UNION (F,{{}}) or y in F )
assume A50: y in UNION (F,{{}}) ; :: thesis: y in F
consider X, Y being set such that
A51: ( X in F & Y in {{}} & y = X \/ Y ) by A50, SETFAM_1:def 4;
Y = {} by A51;
hence y in F by A51; :: thesis: verum

end;

then A52: ( F \/ (UNION (F,{{((len f) + 1),((len f) + 2)}})) = UNION (F,({{}} \/ {{((len f) + 1),((len f) + 2)}})) & (UNION (F,{{((len f) + 2)}})) \/ (UNION (F,{{((len f) + 1)}})) = UNION (F,({{((len f) + 1)}} \/ {{((len f) + 2)}})) ) by Th7;
then reconsider et = ET as Enumeration of F2 by A3, A46, Th7;
A53: F \/ (UNION (F,{{((len f) + 1)}})) = UNION (F,({{}} \/ {{((len f) + 1)}})) by A48, Th7
.= UNION (F,{{},{((len f) + 1)}}) by ENUMSET1:1
.= F1 by A3, ZFMISC_1:24 ;
then reconsider ee1 = EE1 as Enumeration of F1 ;
take ee1 ; :: thesis: ex E2 being Enumeration of F2 st A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,F2)) * E2) = (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F1)) * ee1)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>),A,F1)) * ee1))
take et ; :: thesis: A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,F2)) * et) = (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F1)) * ee1)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>),A,F1)) * ee1))
A54: A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(F \/ (UNION (F,{{((len f) + 1),((len f) + 2)}}))))) * EE12) = A "**" (((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,F)) * the Enumeration of F) ^ ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(UNION (F,{{((len f) + 1),((len f) + 2)}})))) * E12)) by Th81
.= (A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,F)) * the Enumeration of F)) ^ (A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(UNION (F,{{((len f) + 1),((len f) + 2)}})))) * E12)) by Th63
.= (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * the Enumeration of F)) ^ (A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(UNION (F,{{((len f) + 1),((len f) + 2)}})))) * E12)) by Th84, A1, A5, A7
.= (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * the Enumeration of F)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(UNION (F,{{((len f) + 1),((len f) + 2)}})))) * E12)) by Th87, A1, A18
.= A "**" (((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * the Enumeration of F) ^ ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(UNION (F,{{((len f) + 1),((len f) + 2)}})))) * E12)) by Th63
.= A "**" (((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F)) * the Enumeration of F) ^ ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,(UNION (F,{{((len f) + 1)}})))) * E1)) by A34, A28, Th90
.= A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F1)) * ee1) by A53, Th81 ;
A55: A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((UNION (F,{{((len f) + 2)}})) \/ (UNION (F,{{((len f) + 1)}}))))) * E2E1) = A "**" (((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(UNION (F,{{((len f) + 2)}})))) * E2) ^ ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(UNION (F,{{((len f) + 1)}})))) * E1)) by Th81
.= (A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(UNION (F,{{((len f) + 2)}})))) * E2)) ^ (A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(UNION (F,{{((len f) + 1)}})))) * E1)) by Th63
.= (A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(UNION (F,{{((len f) + 2)}})))) * E2)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>),A,(UNION (F,{{((len f) + 1)}})))) * E1)) by Th86, A1, A9, A10
.= (A "**" ((SignGenOp ((f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>),A,(UNION (F,{{((len f) + 2)}})))) * E2)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>),A,(UNION (F,{{((len f) + 1)}})))) * E1)) by Th85, A1, A14, A13
.= (A "**" ((SignGenOp ((f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>),A,F)) * the Enumeration of F)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>),A,(UNION (F,{{((len f) + 1)}})))) * E1)) by A27, Th90, A38
.= A "**" (((SignGenOp ((f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>),A,F)) * the Enumeration of F) ^ ((SignGenOp ((f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>),A,(UNION (F,{{((len f) + 1)}})))) * E1)) by Th63
.= A "**" ((SignGenOp ((f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>),A,F1)) * ee1) by A53, Th81 ;
(SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,F2)) * et = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((F \/ (UNION (F,{{((len f) + 1),((len f) + 2)}}))) \/ ((UNION (F,{{((len f) + 2)}})) \/ (UNION (F,{{((len f) + 1)}})))))) * ET by A3, A46, A52, Th7
.= ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(F \/ (UNION (F,{{((len f) + 1),((len f) + 2)}}))))) * EE12) ^ ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,((UNION (F,{{((len f) + 2)}})) \/ (UNION (F,{{((len f) + 1)}}))))) * E2E1) by Th81 ;
hence A "**" ((SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,F2)) * et) = (A "**" ((SignGenOp ((f ^ <*(A . (d1,d2))*>),A,F1)) * ee1)) ^ (A "**" ((SignGenOp ((f ^ <*(A . (d1,((the_inverseOp_wrt A) . d2)))*>),A,F1)) * ee1)) by A54, A55, Th63; :: thesis: verum