let D be non empty set ; :: thesis: for A being BinOp of D
for d1 being Element of D
for f being FinSequence of D st A is having_a_unity & A is associative & A is having_an_inverseOp holds
for F, Fb being finite set st Fb = UNION (F,(bool {((len f) + 1)})) & union F c= dom f holds
for E1 being Enumeration of Fb ex E2 being Enumeration of Fb st (SignGenOp ((f ^ <*d1*>),A,Fb)) * E1 = (SignGenOp ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,Fb)) * E2
let A be BinOp of D; :: thesis: for d1 being Element of D
for f being FinSequence of D st A is having_a_unity & A is associative & A is having_an_inverseOp holds
for F, Fb being finite set st Fb = UNION (F,(bool {((len f) + 1)})) & union F c= dom f holds
for E1 being Enumeration of Fb ex E2 being Enumeration of Fb st (SignGenOp ((f ^ <*d1*>),A,Fb)) * E1 = (SignGenOp ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,Fb)) * E2
let d1 be Element of D; :: thesis: for f being FinSequence of D st A is having_a_unity & A is associative & A is having_an_inverseOp holds
for F, Fb being finite set st Fb = UNION (F,(bool {((len f) + 1)})) & union F c= dom f holds
for E1 being Enumeration of Fb ex E2 being Enumeration of Fb st (SignGenOp ((f ^ <*d1*>),A,Fb)) * E1 = (SignGenOp ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,Fb)) * E2
let f be FinSequence of D; :: thesis: ( A is having_a_unity & A is associative & A is having_an_inverseOp implies for F, Fb being finite set st Fb = UNION (F,(bool {((len f) + 1)})) & union F c= dom f holds
for E1 being Enumeration of Fb ex E2 being Enumeration of Fb st (SignGenOp ((f ^ <*d1*>),A,Fb)) * E1 = (SignGenOp ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,Fb)) * E2 )
set I = the_inverseOp_wrt A;
assume A1: ( A is having_a_unity & A is associative & A is having_an_inverseOp ) ; :: thesis: for F, Fb being finite set st Fb = UNION (F,(bool {((len f) + 1)})) & union F c= dom f holds
for E1 being Enumeration of Fb ex E2 being Enumeration of Fb st (SignGenOp ((f ^ <*d1*>),A,Fb)) * E1 = (SignGenOp ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,Fb)) * E2
let F, Fb be finite set ; :: thesis: ( Fb = UNION (F,(bool {((len f) + 1)})) & union F c= dom f implies for E1 being Enumeration of Fb ex E2 being Enumeration of Fb st (SignGenOp ((f ^ <*d1*>),A,Fb)) * E1 = (SignGenOp ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,Fb)) * E2 )
assume that
A2: Fb = UNION (F,(bool {((len f) + 1)})) and
A3: union F c= dom f ; :: thesis: for E1 being Enumeration of Fb ex E2 being Enumeration of Fb st (SignGenOp ((f ^ <*d1*>),A,Fb)) * E1 = (SignGenOp ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,Fb)) * E2
let E1 be Enumeration of Fb; :: thesis: ex E2 being Enumeration of Fb st (SignGenOp ((f ^ <*d1*>),A,Fb)) * E1 = (SignGenOp ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,Fb)) * E2
defpred S₁[ object , object ] means ( $2 in dom E1 & ( 1 + (len f) in E1 . $1 implies E1 . $2 = (E1 . $1) \ {(1 + (len f))} ) & ( not 1 + (len f) in E1 . $1 implies E1 . $2 = (E1 . $1) \/ {(1 + (len f))} ) );
A4: rng E1 = Fb by RLAFFIN3:def 1;
A5: for x being object st x in dom E1 holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in dom E1 implies ex y being object st S₁[x,y] )
assume x in dom E1 ; :: thesis: ex y being object st S₁[x,y]
then E1 . x in Fb by A4, FUNCT_1:def 3;
then consider X, Y being set such that
A6: ( X in F & Y in bool {((len f) + 1)} & E1 . x = X \/ Y ) by A2, SETFAM_1:def 4;
1 + (len f) > len f by NAT_1:13;
then A7: not 1 + (len f) in dom f by FINSEQ_3:25;
A8: X c= union F by A6, ZFMISC_1:74;
then A9: not 1 + (len f) in X by A7, A3;

per cases ( Y = {(1 + (len f))} or Y = {} ) by A6, ZFMISC_1:33;

suppose A10: Y = {(1 + (len f))} ; :: thesis: ex y being object st S₁[x,y]

{} c= {((len f) + 1)} ;
then ( (E1 . x) \ {(1 + (len f))} = X & {} in bool {((len f) + 1)} ) by A6, A10, A9, ZFMISC_1:117;
then ((E1 . x) \ {(1 + (len f))}) \/ {} in Fb by A2, A6, SETFAM_1:def 4;
then consider y being object such that
A11: ( y in dom E1 & E1 . y = (E1 . x) \ {(1 + (len f))} ) by A4, FUNCT_1:def 3;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] by A11, A10, A6, ZFMISC_1:136; :: thesis: verum

end;

suppose A12: Y = {} ; :: thesis: ex y being object st S₁[x,y]

{((len f) + 1)} c= {((len f) + 1)} ;
then (E1 . x) \/ {((len f) + 1)} in Fb by A2, A6, A12, SETFAM_1:def 4;
then consider y being object such that
A13: ( y in dom E1 & E1 . y = (E1 . x) \/ {(1 + (len f))} ) by A4, FUNCT_1:def 3;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] by A13, A12, A6, A8, A7, A3; :: thesis: verum

end;

end;

end;

consider p being Function such that
A14: dom p = dom E1 and
A15: for x being object st x in dom E1 holds
S₁[x,p . x] from CLASSES1:sch 1(A5);
rng p c= dom E1

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in dom E1 )
assume y in rng p ; :: thesis: y in dom E1
then ex x being object st
( x in dom p & p . x = y ) by FUNCT_1:def 3;
hence y in dom E1 by A14, A15; :: thesis: verum

end;

then reconsider p = p as Function of (dom E1),(dom E1) by A14, FUNCT_2:2;
dom E1 c= rng p

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom E1 or x in rng p )
assume A16: x in dom E1 ; :: thesis: x in rng p
then E1 . x in Fb by A4, FUNCT_1:def 3;
then consider X, Y being set such that
A17: ( X in F & Y in bool {((len f) + 1)} & E1 . x = X \/ Y ) by A2, SETFAM_1:def 4;
1 + (len f) > len f by NAT_1:13;
then A18: not 1 + (len f) in dom f by FINSEQ_3:25;
A19: X c= union F by A17, ZFMISC_1:74;
then A20: not 1 + (len f) in X by A18, A3;

per cases ( Y = {(1 + (len f))} or Y = {} ) by A17, ZFMISC_1:33;

suppose A21: Y = {(1 + (len f))} ; :: thesis: x in rng p

then A22: 1 + (len f) in E1 . x by A17, ZFMISC_1:136;
{} c= {((len f) + 1)} ;
then ( (E1 . x) \ {(1 + (len f))} = X & {} in bool {((len f) + 1)} ) by A17, A21, A20, ZFMISC_1:117;
then ((E1 . x) \ {(1 + (len f))}) \/ {} in Fb by A2, A17, SETFAM_1:def 4;
then consider z being object such that
A23: ( z in dom E1 & E1 . z = (E1 . x) \ {(1 + (len f))} ) by A4, FUNCT_1:def 3;
not 1 + (len f) in E1 . z by A23, ZFMISC_1:56;
then ( E1 . (p . z) = (E1 . z) \/ {(1 + (len f))} & p . z in dom E1 ) by A23, A15;
then p . z = x by A16, FUNCT_1:def 4, A23, A22, ZFMISC_1:116;
hence x in rng p by A14, A23, FUNCT_1:def 3; :: thesis: verum

end;

suppose A24: Y = {} ; :: thesis: x in rng p

then A25: not 1 + (len f) in E1 . x by A17, A19, A18, A3;
{((len f) + 1)} c= {((len f) + 1)} ;
then (E1 . x) \/ {((len f) + 1)} in Fb by A17, A24, A2, SETFAM_1:def 4;
then consider z being object such that
A26: ( z in dom E1 & E1 . z = (E1 . x) \/ {(1 + (len f))} ) by A4, FUNCT_1:def 3;
1 + (len f) in E1 . z by A26, ZFMISC_1:136;
then A27: ( E1 . (p . z) = (E1 . z) \ {(1 + (len f))} & p . z in dom E1 ) by A26, A15;
then E1 . (p . z) = E1 . x by A26, A25, ZFMISC_1:117;
then p . z = x by A27, A16, FUNCT_1:def 4;
hence x in rng p by A14, A26, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

then dom E1 = rng p ;
then A28: ( p is onto & card (dom E1) = card (dom E1) ) by FUNCT_2:def 3;
then p is one-to-one by FINSEQ_4:63;
then reconsider p = p as Permutation of (dom E1) by A28;
reconsider E1p = E1 * p as Enumeration of Fb by Th109;
take E1p ; :: thesis: (SignGenOp ((f ^ <*d1*>),A,Fb)) * E1 = (SignGenOp ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,Fb)) * E1p
A29: ( len ((SignGenOp ((f ^ <*d1*>),A,Fb)) * E1) = len E1 & len E1 = card Fb & len ((SignGenOp ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,Fb)) * E1p) = len E1p & len E1p = card Fb ) by CARD_1:def 7;
for i being Nat st 1 <= i & i <= len ((SignGenOp ((f ^ <*d1*>),A,Fb)) * E1) holds
((SignGenOp ((f ^ <*d1*>),A,Fb)) * E1) . i = ((SignGenOp ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,Fb)) * E1p) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len ((SignGenOp ((f ^ <*d1*>),A,Fb)) * E1) implies ((SignGenOp ((f ^ <*d1*>),A,Fb)) * E1) . i = ((SignGenOp ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,Fb)) * E1p) . i )
assume A30: ( 1 <= i & i <= len ((SignGenOp ((f ^ <*d1*>),A,Fb)) * E1) ) ; :: thesis: ((SignGenOp ((f ^ <*d1*>),A,Fb)) * E1) . i = ((SignGenOp ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,Fb)) * E1p) . i
( i in dom ((SignGenOp ((f ^ <*d1*>),A,Fb)) * E1) & i in dom ((SignGenOp ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,Fb)) * E1p) ) by A29, A30, FINSEQ_3:25;
then A31: ( ((SignGenOp ((f ^ <*d1*>),A,Fb)) * E1) . i = SignGen ((f ^ <*d1*>),A,(E1 . i)) & ((SignGenOp ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,Fb)) * E1p) . i = SignGen ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,(E1p . i)) ) by Th80;
i in dom E1p by A30, A29, FINSEQ_3:25;
then A32: ( i in dom p & E1p . i = E1 . (p . i) ) by FUNCT_1:11, FUNCT_1:12;
A33: ( len (f ^ <*d1*>) = 1 + (len f) & 1 + (len f) = len (f ^ <*((the_inverseOp_wrt A) . d1)*>) ) by FINSEQ_2:16;
A34: ( (f ^ <*d1*>) | (len f) = f & f = (f ^ <*((the_inverseOp_wrt A) . d1)*>) | (len f) ) ;
A35: ( (f ^ <*d1*>) . (1 + (len f)) = d1 & (f ^ <*((the_inverseOp_wrt A) . d1)*>) . (1 + (len f)) = (the_inverseOp_wrt A) . d1 ) ;
1 + (len f) > len f by NAT_1:13;
then not 1 + (len f) in dom f by FINSEQ_3:25;
then A36: {(1 + (len f))} misses dom f by ZFMISC_1:50;

per cases ( 1 + (len f) in E1 . i or not 1 + (len f) in E1 . i ) ;

suppose A37: 1 + (len f) in E1 . i ; :: thesis: ((SignGenOp ((f ^ <*d1*>),A,Fb)) * E1) . i = ((SignGenOp ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,Fb)) * E1p) . i

E1 . (p . i) = (E1 . i) \ {(1 + (len f))} by A37, A15, A32;
then not 1 + (len f) in E1p . i by A32, ZFMISC_1:56;
then A38: SignGen ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,(E1p . i)) = (SignGen (f,A,(E1p . i))) ^ <*((the_inverseOp_wrt A) . d1)*> by A33, A34, A35, Th74;
(E1p . i) /\ (dom f) = ((E1 . i) \ {(1 + (len f))}) /\ (dom f) by A37, A15, A32
.= ((dom f) /\ (E1 . i)) \ ((dom f) /\ {(1 + (len f))}) by XBOOLE_1:50
.= (dom f) /\ (E1 . i) by A36 ;
then SignGen (f,A,(E1p . i)) = SignGen (f,A,((E1 . i) /\ (dom f))) by Th89
.= SignGen (f,A,(E1 . i)) by Th89 ;
hence ((SignGenOp ((f ^ <*d1*>),A,Fb)) * E1) . i = ((SignGenOp ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,Fb)) * E1p) . i by A37, A33, A34, A35, Th73, A38, A31; :: thesis: verum

end;

suppose A39: not 1 + (len f) in E1 . i ; :: thesis: ((SignGenOp ((f ^ <*d1*>),A,Fb)) * E1) . i = ((SignGenOp ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,Fb)) * E1p) . i

E1 . (p . i) = (E1 . i) \/ {(1 + (len f))} by A39, A15, A32;
then 1 + (len f) in E1p . i by A32, ZFMISC_1:136;
then A40: SignGen ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,(E1p . i)) = (SignGen (f,A,(E1p . i))) ^ <*((the_inverseOp_wrt A) . ((the_inverseOp_wrt A) . d1))*> by A33, A34, A35, Th73;
A41: (the_inverseOp_wrt A) . ((the_inverseOp_wrt A) . d1) = d1 by A1, FINSEQOP:62;
(E1p . i) /\ (dom f) = (dom f) /\ ((E1 . i) \/ {(1 + (len f))}) by A39, A15, A32
.= ((dom f) /\ (E1 . i)) \/ ((dom f) /\ {(1 + (len f))}) by XBOOLE_1:23
.= (dom f) /\ (E1 . i) by A36 ;
then SignGen (f,A,(E1p . i)) = SignGen (f,A,((E1 . i) /\ (dom f))) by Th89
.= SignGen (f,A,(E1 . i)) by Th89 ;
hence ((SignGenOp ((f ^ <*d1*>),A,Fb)) * E1) . i = ((SignGenOp ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,Fb)) * E1p) . i by A39, A33, A34, A35, Th74, A40, A31, A41; :: thesis: verum

end;

end;

end;

hence (SignGenOp ((f ^ <*d1*>),A,Fb)) * E1 = (SignGenOp ((f ^ <*((the_inverseOp_wrt A) . d1)*>),A,Fb)) * E1p by A29; :: thesis: verum