let D be non empty set ; :: thesis: for A, M being BinOp of D
for f being FinSequence of D st M is commutative & M is associative & A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is_distributive_wrt A holds
for E being Enumeration of bool {2}
for CE being non-empty non empty FinSequence of D * st CE = (SignGenOp (f,A,(bool {2}))) * E & len f = 2 holds
ex S being Element of Fin (dom (App CE)) st
( S = {<*1,1*>,<*2,2*>} & SignGenOp (f,M,A,{2}) = A $$ (S,(M "**" (App CE))) )
let A, M be BinOp of D; :: thesis: for f being FinSequence of D st M is commutative & M is associative & A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is_distributive_wrt A holds
for E being Enumeration of bool {2}
for CE being non-empty non empty FinSequence of D * st CE = (SignGenOp (f,A,(bool {2}))) * E & len f = 2 holds
ex S being Element of Fin (dom (App CE)) st
( S = {<*1,1*>,<*2,2*>} & SignGenOp (f,M,A,{2}) = A $$ (S,(M "**" (App CE))) )
let f be FinSequence of D; :: thesis: ( M is commutative & M is associative & A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp & M is_distributive_wrt A implies for E being Enumeration of bool {2}
for CE being non-empty non empty FinSequence of D * st CE = (SignGenOp (f,A,(bool {2}))) * E & len f = 2 holds
ex S being Element of Fin (dom (App CE)) st
( S = {<*1,1*>,<*2,2*>} & SignGenOp (f,M,A,{2}) = A $$ (S,(M "**" (App CE))) ) )
assume that
A1: ( M is commutative & M is associative ) and
A2: ( A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp ) and
A3: M is_distributive_wrt A ; :: thesis: for E being Enumeration of bool {2}
for CE being non-empty non empty FinSequence of D * st CE = (SignGenOp (f,A,(bool {2}))) * E & len f = 2 holds
ex S being Element of Fin (dom (App CE)) st
( S = {<*1,1*>,<*2,2*>} & SignGenOp (f,M,A,{2}) = A $$ (S,(M "**" (App CE))) )
let E be Enumeration of bool {2}; :: thesis: for CE being non-empty non empty FinSequence of D * st CE = (SignGenOp (f,A,(bool {2}))) * E & len f = 2 holds
ex S being Element of Fin (dom (App CE)) st
( S = {<*1,1*>,<*2,2*>} & SignGenOp (f,M,A,{2}) = A $$ (S,(M "**" (App CE))) )
let CE be non-empty non empty FinSequence of D * ; :: thesis: ( CE = (SignGenOp (f,A,(bool {2}))) * E & len f = 2 implies ex S being Element of Fin (dom (App CE)) st
( S = {<*1,1*>,<*2,2*>} & SignGenOp (f,M,A,{2}) = A $$ (S,(M "**" (App CE))) ) )
assume A4: ( CE = (SignGenOp (f,A,(bool {2}))) * E & len f = 2 ) ; :: thesis: ex S being Element of Fin (dom (App CE)) st
( S = {<*1,1*>,<*2,2*>} & SignGenOp (f,M,A,{2}) = A $$ (S,(M "**" (App CE))) )
set C = SignGenOp (f,A,(bool {2}));
set I = the_inverseOp_wrt A;
( 1 in dom f & 2 in dom f ) by A4, FINSEQ_3:25;
then ( f . 1 in rng f & f . 2 in rng f & rng f c= D ) by FUNCT_1:def 3;
then reconsider f1 = f . 1, f2 = f . 2 as Element of D ;
( M . (f1,(A . (f1,((the_inverseOp_wrt A) . f2)))) = A . ((M . (f1,f1)),(M . (f1,((the_inverseOp_wrt A) . f2)))) & M . (f2,(A . (f1,((the_inverseOp_wrt A) . f2)))) = A . ((M . (f2,f1)),(M . (f2,((the_inverseOp_wrt A) . f2)))) ) by A3, BINOP_1:11;
then A5: M . ((A . (f1,f2)),(A . (f1,((the_inverseOp_wrt A) . f2)))) = A . ((A . ((M . (f1,f1)),(M . (f1,((the_inverseOp_wrt A) . f2))))),(A . ((M . (f2,f1)),(M . (f2,((the_inverseOp_wrt A) . f2)))))) by A3, BINOP_1:def 10, BINOP_1:def 11
.= A . ((M . (f1,f1)),(A . ((M . (f1,((the_inverseOp_wrt A) . f2))),(A . ((M . (f2,f1)),(M . (f2,((the_inverseOp_wrt A) . f2)))))))) by A2, BINOP_1:def 3
.= A . ((M . (f1,f1)),(A . ((A . ((M . (f1,((the_inverseOp_wrt A) . f2))),(M . (f2,f1)))),(M . (f2,((the_inverseOp_wrt A) . f2)))))) by A2, BINOP_1:def 3
.= A . ((M . (f1,f1)),(A . ((A . (((the_inverseOp_wrt A) . (M . (f1,f2))),(M . (f2,f1)))),(M . (f2,((the_inverseOp_wrt A) . f2)))))) by A3, A2, FINSEQOP:67
.= A . ((M . (f1,f1)),(A . ((A . (((the_inverseOp_wrt A) . (M . (f1,f2))),(M . (f1,f2)))),(M . (f2,((the_inverseOp_wrt A) . f2)))))) by A1, BINOP_1:def 2
.= A . ((M . (f1,f1)),(A . ((the_unity_wrt A),(M . (f2,((the_inverseOp_wrt A) . f2)))))) by A2, FINSEQOP:59
.= A . ((M . (f1,f1)),(M . (f2,((the_inverseOp_wrt A) . f2)))) by A2, SETWISEO:15 ;
A6: bool {2} = {{},{2}} by ZFMISC_1:24;
then card (bool {2}) = 2 by CARD_2:57;
then A7: ( len CE = len E & len E = len f ) by A4, CARD_1:def 7;
A8: ( 1 in dom CE & 1 in dom E & 2 in dom CE & 2 in dom E ) by A7, A4, FINSEQ_3:25;
then A9: ( CE . 1 = (SignGenOp (f,A,(bool {2}))) . (E . 1) & E . 1 in rng E & CE . 2 = (SignGenOp (f,A,(bool {2}))) . (E . 2) & E . 2 in rng E ) by A4, FUNCT_1:12, FUNCT_1:def 3;
then A10: ( CE . 1 = SignGen (f,A,(E . 1)) & CE . 2 = SignGen (f,A,(E . 2)) ) by Def12;
then A11: ( len (CE . 1) = len f & len (CE . 2) = len f ) by CARD_1:def 7;
A12: {<*1,1*>,<*2,2*>} c= doms CE

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {<*1,1*>,<*2,2*>} or x in doms CE )
assume A13: x in {<*1,1*>,<*2,2*>} ; :: thesis: x in doms CE
then A14: ( x = <*1,1*> or x = <*2,2*> ) by TARSKI:def 2;
reconsider x = x as FinSequence by A13;
A15: len x = 2 by A14, FINSEQ_1:44;
for i being Nat st i in dom x holds
x . i in dom (CE . i)

proof

let i be Nat; :: thesis: ( i in dom x implies x . i in dom (CE . i) )
assume A16: i in dom x ; :: thesis: x . i in dom (CE . i)
A17: ( 1 <= i & i <= 2 ) by A16, A15, FINSEQ_3:25;
then ( i < 2 or i = 2 ) by XXREAL_0:1;
then A18: ( i = 1 or i = 2 ) by A17, NAT_1:23;
then ( x . i = 1 or x . i = 2 ) by A14;
hence x . i in dom (CE . i) by A18, A11, A4, FINSEQ_3:25; :: thesis: verum

end;

hence x in doms CE by A15, A4, A7, Th47; :: thesis: verum

end;

then {<*1,1*>,<*2,2*>} c= dom (App CE) by Def9;
then reconsider S = {<*1,1*>,<*2,2*>} as Element of Fin (dom (App CE)) by FINSUB_1:def 5;
take S ; :: thesis: ( S = {<*1,1*>,<*2,2*>} & SignGenOp (f,M,A,{2}) = A $$ (S,(M "**" (App CE))) )
thus S = {<*1,1*>,<*2,2*>} ; :: thesis: SignGenOp (f,M,A,{2}) = A $$ (S,(M "**" (App CE)))
A19: SignGenOp (f,M,A,{2}) = A . ((M . (f1,f1)),(M . (f2,((the_inverseOp_wrt A) . f2)))) by A5, A4, A1, Th140;
( <*1,1*> in {<*1,1*>,<*2,2*>} & <*2,2*> in {<*1,1*>,<*2,2*>} ) by TARSKI:def 2;
then reconsider s1 = <*1,1*>, s2 = <*2,2*> as Element of dom (App CE) by A12, Def9;
( s1 . 1 = 1 & s2 . 1 = 2 ) ;
then A20: s1 <> s2 ;
A21: A $$ (S,(M "**" (App CE))) = A . (((M "**" (App CE)) . s1),((M "**" (App CE)) . s2)) by A20, A2, SETWOP_2:1
.= A . ((M "**" ((App CE) . s1)),((M "**" (App CE)) . s2)) by Def10
.= A . ((M "**" ((App CE) . s1)),(M "**" ((App CE) . s2))) by Def10 ;
A22: ( len ((App CE) . s1) = len s1 & len s1 = 2 ) by Def9, CARD_1:def 7;
A23: ( len ((App CE) . s2) = len s2 & len s2 = 2 ) by Def9, CARD_1:def 7;
A26: E . 1 <> E . 2 by A8, FUNCT_1:def 4;

per cases ( E . 1 = {} or E . 1 = {2} ) by A6, A9, TARSKI:def 2;

suppose A27: E . 1 = {} ; :: thesis: SignGenOp (f,M,A,{2}) = A $$ (S,(M "**" (App CE)))

then A28: E . 2 = {2} by A26, A6, A9, TARSKI:def 2;
for k being Nat st 1 <= k & k <= 2 holds
((App CE) . s1) . k = <*f1,f1*> . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= 2 implies ((App CE) . s1) . k = <*f1,f1*> . k )
assume A29: ( 1 <= k & k <= 2 ) ; :: thesis: ((App CE) . s1) . k = <*f1,f1*> . k
A30: k in dom s1 by A29, A22, FINSEQ_3:25;
then A31: ((App CE) . s1) . k = (CE . k) . (s1 . k) by Def9;
( k < 2 or k = 2 ) by A29, XXREAL_0:1;

per cases then ( k = 1 or k = 2 ) by A29, NAT_1:23;

suppose A32: k = 1 ; :: thesis: ((App CE) . s1) . k = <*f1,f1*> . k

then (CE . k) . (s1 . k) = f1 by A27, A10, Th71;
hence ((App CE) . s1) . k = <*f1,f1*> . k by A30, Def9, A32; :: thesis: verum

end;

suppose A33: k = 2 ; :: thesis: ((App CE) . s1) . k = <*f1,f1*> . k

len (SignGen (f,A,{2})) = len f by CARD_1:def 7;
then ( 1 in dom (SignGen (f,A,{2})) & not 1 in {2} ) by A4, FINSEQ_3:25, TARSKI:def 1;
then (SignGen (f,A,{2})) . 1 = f . 1 by Def11;
hence ((App CE) . s1) . k = <*f1,f1*> . k by A31, A28, A10, A33; :: thesis: verum

end;

end;

end;

then (App CE) . s1 = <*f1,f1*> by CARD_1:def 7, A22;
then A34: M "**" ((App CE) . s1) = M . (f1,f1) by FINSOP_1:12;
for k being Nat st 1 <= k & k <= 2 holds
((App CE) . s2) . k = <*f2,((the_inverseOp_wrt A) . f2)*> . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= 2 implies ((App CE) . s2) . k = <*f2,((the_inverseOp_wrt A) . f2)*> . k )
assume A35: ( 1 <= k & k <= 2 ) ; :: thesis: ((App CE) . s2) . k = <*f2,((the_inverseOp_wrt A) . f2)*> . k
k in dom s2 by A35, A23, FINSEQ_3:25;
then A36: ((App CE) . s2) . k = (CE . k) . (s2 . k) by Def9;
( k < 2 or k = 2 ) by A35, XXREAL_0:1;

per cases then ( k = 1 or k = 2 ) by A35, NAT_1:23;

suppose k = 1 ; :: thesis: ((App CE) . s2) . k = <*f2,((the_inverseOp_wrt A) . f2)*> . k

hence ((App CE) . s2) . k = <*f2,((the_inverseOp_wrt A) . f2)*> . k by A36, Th71, A27, A10; :: thesis: verum

end;

suppose A37: k = 2 ; :: thesis: ((App CE) . s2) . k = <*f2,((the_inverseOp_wrt A) . f2)*> . k

len (SignGen (f,A,{2})) = len f by CARD_1:def 7;
then ( 2 in dom (SignGen (f,A,{2})) & 2 in {2} ) by A4, FINSEQ_3:25, TARSKI:def 1;
then (SignGen (f,A,{2})) . 2 = (the_inverseOp_wrt A) . f2 by Def11;
hence ((App CE) . s2) . k = <*f2,((the_inverseOp_wrt A) . f2)*> . k by A36, A28, A10, A37; :: thesis: verum

end;

end;

end;

then (App CE) . s2 = <*f2,((the_inverseOp_wrt A) . f2)*> by CARD_1:def 7, A23;
hence SignGenOp (f,M,A,{2}) = A $$ (S,(M "**" (App CE))) by A19, A21, A34, FINSOP_1:12; :: thesis: verum

end;

suppose A38: E . 1 = {2} ; :: thesis: SignGenOp (f,M,A,{2}) = A $$ (S,(M "**" (App CE)))

then A39: E . 2 = {} by A26, A6, A9, TARSKI:def 2;
for k being Nat st 1 <= k & k <= 2 holds
((App CE) . s1) . k = <*f1,f1*> . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= 2 implies ((App CE) . s1) . k = <*f1,f1*> . k )
assume A40: ( 1 <= k & k <= 2 ) ; :: thesis: ((App CE) . s1) . k = <*f1,f1*> . k
k in dom s1 by A40, A22, FINSEQ_3:25;
then A41: ((App CE) . s1) . k = (CE . k) . (s1 . k) by Def9;
( k < 2 or k = 2 ) by A40, XXREAL_0:1;

per cases then ( k = 2 or k = 1 ) by A40, NAT_1:23;

suppose A42: k = 2 ; :: thesis: ((App CE) . s1) . k = <*f1,f1*> . k

then (CE . k) . (s1 . k) = f1 by A39, A10, Th71;
hence ((App CE) . s1) . k = <*f1,f1*> . k by A41, A42; :: thesis: verum

end;

suppose A43: k = 1 ; :: thesis: ((App CE) . s1) . k = <*f1,f1*> . k

len (SignGen (f,A,{2})) = len f by CARD_1:def 7;
then ( 1 in dom (SignGen (f,A,{2})) & not 1 in {2} ) by A4, FINSEQ_3:25, TARSKI:def 1;
hence ((App CE) . s1) . k = <*f1,f1*> . k by A41, A38, A10, A43, Def11; :: thesis: verum

end;

end;

end;

then (App CE) . s1 = <*f1,f1*> by CARD_1:def 7, A22;
then A44: M "**" ((App CE) . s1) = M . (f1,f1) by FINSOP_1:12;
for k being Nat st 1 <= k & k <= 2 holds
((App CE) . s2) . k = <*((the_inverseOp_wrt A) . f2),f2*> . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= 2 implies ((App CE) . s2) . k = <*((the_inverseOp_wrt A) . f2),f2*> . k )
assume A45: ( 1 <= k & k <= 2 ) ; :: thesis: ((App CE) . s2) . k = <*((the_inverseOp_wrt A) . f2),f2*> . k
k in dom s2 by A45, A23, FINSEQ_3:25;
then A46: ((App CE) . s2) . k = (CE . k) . (s2 . k) by Def9;
( k < 2 or k = 2 ) by A45, XXREAL_0:1;

per cases then ( k = 2 or k = 1 ) by A45, NAT_1:23;

suppose A47: k = 2 ; :: thesis: ((App CE) . s2) . k = <*((the_inverseOp_wrt A) . f2),f2*> . k

then CE . k = SignGen (f,A,{}) by A38, A26, A6, A9, TARSKI:def 2, A10;
then (CE . k) . (s2 . k) = f2 by Th71, A47;
hence ((App CE) . s2) . k = <*((the_inverseOp_wrt A) . f2),f2*> . k by A46, A47; :: thesis: verum

end;

suppose A48: k = 1 ; :: thesis: ((App CE) . s2) . k = <*((the_inverseOp_wrt A) . f2),f2*> . k

len (SignGen (f,A,{2})) = len f by CARD_1:def 7;
then ( 2 in dom (SignGen (f,A,{2})) & 2 in {2} ) by A4, FINSEQ_3:25, TARSKI:def 1;
hence ((App CE) . s2) . k = <*((the_inverseOp_wrt A) . f2),f2*> . k by A46, A38, A10, A48, Def11; :: thesis: verum

end;

end;

end;

then A49: (App CE) . s2 = <*((the_inverseOp_wrt A) . f2),f2*> by CARD_1:def 7, A23;
A $$ (S,(M "**" (App CE))) = A . ((M . (f1,f1)),(M . (((the_inverseOp_wrt A) . f2),f2))) by A21, A44, A49, FINSOP_1:12
.= A . ((M . (f1,f1)),(M . (f2,((the_inverseOp_wrt A) . f2)))) by A1, BINOP_1:def 2 ;
hence SignGenOp (f,M,A,{2}) = A $$ (S,(M "**" (App CE))) by A5, A4, A1, Th140; :: thesis: verum

end;

end;