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 & len f = 2 holds
SignGenOp (f,M,A,{2}) = M . ((A . ((f . 1),(f . 2))),(A . ((f . 1),((the_inverseOp_wrt A) . (f . 2)))))
let A, M be BinOp of D; :: thesis: for f being FinSequence of D st M is commutative & M is associative & len f = 2 holds
SignGenOp (f,M,A,{2}) = M . ((A . ((f . 1),(f . 2))),(A . ((f . 1),((the_inverseOp_wrt A) . (f . 2)))))
let f be FinSequence of D; :: thesis: ( M is commutative & M is associative & len f = 2 implies SignGenOp (f,M,A,{2}) = M . ((A . ((f . 1),(f . 2))),(A . ((f . 1),((the_inverseOp_wrt A) . (f . 2))))) )
assume A1: ( M is commutative & M is associative & len f = 2 ) ; :: thesis: SignGenOp (f,M,A,{2}) = M . ((A . ((f . 1),(f . 2))),(A . ((f . 1),((the_inverseOp_wrt A) . (f . 2)))))
A2: bool {2} = {{},{2}} by ZFMISC_1:24;
set E = (1,2) --> ({},{2});
set I = the_inverseOp_wrt A;
A3: ( dom ((1,2) --> ({},{2})) = {1,2} & {1,2} = Seg 2 ) by FUNCT_4:62, FINSEQ_1:2;
then reconsider E = (1,2) --> ({},{2}) as FinSequence by FINSEQ_1:def 2;
A4: rng E = {{},{2}} by FUNCT_4:64;
( 1 .--> {} = {1} --> {} & 2 .--> {2} = {2} --> {2} ) by FUNCOP_1:def 9;
then ( rng (1 .--> {}) = {{}} & rng (2 .--> {2}) = {{2}} ) by FUNCOP_1:8;
then (1 .--> {}) +* (2 .--> {2}) is one-to-one by FUNCT_4:92, ZFMISC_1:11;
then E is one-to-one by FUNCT_4:def 4;
then reconsider E = E as Enumeration of bool {2} by A4, A2, RLAFFIN3:def 1;
set C = SignGenOp (f,A,(bool {2}));
card (bool {2}) = 2 by A2, CARD_2:57;
then ( len ((SignGenOp (f,A,(bool {2}))) * E) = len E & len E = 2 ) by CARD_1:def 7;
then A5: dom ((SignGenOp (f,A,(bool {2}))) * E) = dom E by FINSEQ_3:30;
then ( 1 in dom ((SignGenOp (f,A,(bool {2}))) * E) & 2 in dom ((SignGenOp (f,A,(bool {2}))) * E) ) by A3;
then reconsider O = 1, T = 2 as Element of [#] (dom ((SignGenOp (f,A,(bool {2}))) * E)) ;
E . O = {} by FUNCT_4:63;
then ( ((SignGenOp (f,A,(bool {2}))) * E) . O = (SignGenOp (f,A,(bool {2}))) . {} & {} in bool {2} ) by FUNCT_1:12, A2, TARSKI:def 2;
then ((SignGenOp (f,A,(bool {2}))) * E) . O = SignGen (f,A,{}) by Def12;
then ((SignGenOp (f,A,(bool {2}))) * E) . O = f by Th71;
then (A "**" ((SignGenOp (f,A,(bool {2}))) * E)) . O = A "**" f by Def10;
then A6: (A "**" ((SignGenOp (f,A,(bool {2}))) * E)) . O = A . ((f . 1),(f . 2)) by A1, FINSOP_1:21;
not f is empty by A1;
then A7: f | 1 = <*(f . 1)*> by FINSEQ_5:20;
then ( dom (f | 1) = Seg 1 & Seg 1 = {1} ) by FINSEQ_1:2, FINSEQ_1:38;
then A8: SignGen ((f | 1),A,{2}) = <*(f . 1)*> by A7, Th70, ZFMISC_1:11;
E . T = {2} by FUNCT_4:63;
then ( ((SignGenOp (f,A,(bool {2}))) * E) . T = (SignGenOp (f,A,(bool {2}))) . {2} & {2} in bool {2} ) by FUNCT_1:12;
then ( ((SignGenOp (f,A,(bool {2}))) * E) . T = SignGen (f,A,{2}) & 1 + 1 in {2} ) by Def12, TARSKI:def 1;
then ((SignGenOp (f,A,(bool {2}))) * E) . T = <*(f . 1),((the_inverseOp_wrt A) . (f . 2))*> by A8, A1, Th73;
then A9: ( len (((SignGenOp (f,A,(bool {2}))) * E) . T) = 2 & (((SignGenOp (f,A,(bool {2}))) * E) . T) . 1 = f . 1 & (((SignGenOp (f,A,(bool {2}))) * E) . T) . 2 = (the_inverseOp_wrt A) . (f . 2) ) by FINSEQ_1:44;
(A "**" ((SignGenOp (f,A,(bool {2}))) * E)) . T = A "**" (((SignGenOp (f,A,(bool {2}))) * E) . T) by Def10;
then A10: (A "**" ((SignGenOp (f,A,(bool {2}))) * E)) . T = A . ((f . 1),((the_inverseOp_wrt A) . (f . 2))) by A9, FINSOP_1:21;
SignGenOp (f,M,A,{2}) = M $$ (([#] (dom ((SignGenOp (f,A,(bool {2}))) * E))),(A "**" ((SignGenOp (f,A,(bool {2}))) * E))) by A1, Def13;
hence SignGenOp (f,M,A,{2}) = M . ((A . ((f . 1),(f . 2))),(A . ((f . 1),((the_inverseOp_wrt A) . (f . 2))))) by A6, A10, A1, A5, A3, SETWOP_2:1; :: thesis: verum