let D be non empty set ; :: thesis:
let A, M be BinOp of D; :: thesis:
let d1, d2 be Element of D; :: thesis:
let f be FinSequence of D; :: thesis:
let F1 be finite set ; :: thesis:
assume A1: ( A is commutative & A is associative & A is having_a_unity & A is having_an_inverseOp ) ; :: thesis:
set I = the_inverseOp_wrt A;
set fDD = (f ^ <*d1*>) ^ <*d2*>;
set fID = (f ^ <*((the_inverseOp_wrt A) . d1)*>) ^ <*d2*>;
let E1 be Enumeration of F1; :: thesis:
assume A2: union F1 c= Seg (1 + (len f)) ; :: thesis:
let Ee be Enumeration of Ext (F1,(1 + (len f)),(2 + (len f))); :: thesis:
let Es be Enumeration of swap (F1,(1 + (len f)),(2 + (len f))); :: thesis:
assume A3: ( Ee = Ext (E1,(1 + (len f)),(2 + (len f))) & Es = Swap (E1,(1 + (len f)),(2 + (len f))) ) ; :: thesis:
let CFe, CFs be non-empty non empty FinSequence of D * ; :: thesis:
assume A4: ( CFe = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext (F1,(1 + (len f)),(2 + (len f)))))) * Ee & CFs = (SignGenOp (((f ^ <*((the_inverseOp_wrt A) . d1)*>) ^ <*d2*>),A,(swap (F1,(1 + (len f)),(2 + (len f)))))) * Es ) ; :: thesis:
defpred S₁[ Nat] means for S1 being Element of Fin (dom (App CFe))
for S2 being Element of Fin (dom (App CFs)) st S1 = S2 & card S1 = $1 holds
A $$ (S1,(M "**" (App CFe))) = A $$ (S2,(M "**" (App CFs)));
A5: S₁[ 0 ]

proof

let S1 be Element of Fin (dom (App CFe)); :: thesis:
let S2 be Element of Fin (dom (App CFs)); :: thesis:
assume ( S1 = S2 & card S1 = 0 ) ; :: thesis:
then A6: ( S1 = {}. (dom (App CFe)) & S2 = {}. (dom (App CFs)) ) ;
hence A $$ (S1,(M "**" (App CFe))) = the_unity_wrt A by A1, SETWISEO:31
.= A $$ (S2,(M "**" (App CFs))) by A1, A6, SETWISEO:31 ;
:: thesis:

end;

A7: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
set n1 = n + 1;
assume A8: S₁[n] ; :: thesis:
let S1 be Element of Fin (dom (App CFe)); :: thesis:
let S2 be Element of Fin (dom (App CFs)); :: thesis:
assume A9: ( S1 = S2 & card S1 = n + 1 ) ; :: thesis:
consider s1 being object such that
A10: s1 in S1 by A9, XBOOLE_0:def 1, XBOOLE_0:def 2;
set S11 = S1 \ {s1};
set S22 = S2 \ {s1};
A11: ( S1 c= dom (App CFe) & S2 c= dom (App CFs) ) by FINSUB_1:def 5;
then reconsider s1 = s1 as Element of dom (App CFe) by A10;
reconsider s2 = s1 as Element of dom (App CFs) by A9, A10, A11;
A12: ( S1 \ {s1} c= dom (App CFe) & S2 \ {s1} c= dom (App CFs) ) by A11;
then reconsider S11 = S1 \ {s1} as Element of Fin (dom (App CFe)) by FINSUB_1:def 5;
reconsider S22 = S2 \ {s1} as Element of Fin (dom (App CFs)) by A12, FINSUB_1:def 5;
A13: ( S1 = S11 \/ {.s1.} & S2 = S22 \/ {.s2.} ) by A9, A10, ZFMISC_1:116;
A14: ( not s1 in S11 & not s2 in S22 ) by ZFMISC_1:56;
A15: card S11 = n by A9, A10, STIRL2_1:55;
A16: ( (M "**" (App CFe)) . s1 = M "**" ((App CFe) . s1) & (M "**" (App CFs)) . s2 = M "**" ((App CFs) . s2) ) by Def10;
A17: ( len ((App CFe) . s1) = len s1 & len s1 = len ((App CFs) . s2) ) by Def9;
for i being Nat st 1 <= i & i <= len s1 holds
((App CFe) . s1) . i = ((App CFs) . s2) . i

proof

per cases ;

suppose A33: 1 + (len f) in E1 . i ; :: thesis:

then A34: ( Ee . i = (E1 . i) \/ {(2 + (len f))} & Es . i = ((E1 . i) \ {(1 + (len f))}) \/ {(2 + (len f))} ) by A19, A3, Def4, Def5;

per cases by A21, A28, A25, FINSEQ_1:25;

suppose A35: s1 . i in dom f ; :: thesis:

then A36: ( ((f ^ <*d1*>) ^ <*d2*>) . s1i = f . s1i & ((f ^ <*((the_inverseOp_wrt A) . d1)*>) ^ <*d2*>) . s1i = f . s1i ) by A28, A31, FINSEQ_1:def 7;
s1i <= len f by A35, FINSEQ_3:25;
then A37: s1i < (len f) + 1 by NAT_1:13;
then A38: s1i < ((len f) + 1) + 1 by NAT_1:13;

per cases ;

suppose A39: s1i in Ee . i ; :: thesis:

then A40: (CFe . i) . s1i = (the_inverseOp_wrt A) . (((f ^ <*d1*>) ^ <*d2*>) . s1i) by A20, A25, Def11;
s1i in (E1 . i) \ {(1 + (len f))} by A37, ZFMISC_1:56, ZFMISC_1:136, A34, A38, A39;
then s1i in Es . i by A34, ZFMISC_1:136;
hence ((App CFe) . s1) . i = ((App CFs) . s2) . i by A24, A36, A40, A25, A22, Def11; :: thesis:

end;

suppose A41: not s1 . i in Ee . i ; :: thesis:

then A42: (CFe . i) . (s1 . i) = ((f ^ <*d1*>) ^ <*d2*>) . (s1 . i) by A20, A25, Def11;
not s1i in (E1 . i) \ {(1 + (len f))} by A34, A41, ZFMISC_1:136;
then not s1i in Es . i by A34, A38, ZFMISC_1:136;
hence ((App CFe) . s1) . i = ((App CFs) . s2) . i by A24, A36, A42, A25, A22, Def11; :: thesis:

end;

suppose ex k being Nat st
( k in dom <*d1,d2*> & s1 . i = (len f) + k ) ; :: thesis:

then consider k being Nat such that
A43: ( k in dom <*d1,d2*> & s1 . i = (len f) + k ) ;

per cases by A43, A26, TARSKI:def 2;

suppose A44: k = 1 ; :: thesis:

then s1i in Ee . i by A33, A43, A34, XBOOLE_0:def 3;
then A45: (CFe . i) . s1i = (the_inverseOp_wrt A) . d1 by A29, A43, A44, A20, A25, Def11;
A46: s1i <> 2 + (len f) by A43, A44;
not s1i in (E1 . i) \ {(1 + (len f))} by ZFMISC_1:56, A43, A44;
then not s1i in Es . i by A46, A34, ZFMISC_1:136;
hence ((App CFe) . s1) . i = ((App CFs) . s2) . i by A24, A45, A43, A44, A32, A25, A22, Def11; :: thesis:

end;

suppose A47: k = 2 ; :: thesis:

then s1i in Ee . i by A43, A34, ZFMISC_1:136;
then A48: (CFe . i) . s1i = (the_inverseOp_wrt A) . d2 by A29, A43, A47, A20, A25, Def11;
s1i in Es . i by A34, ZFMISC_1:136, A43, A47;
hence ((App CFe) . s1) . i = ((App CFs) . s2) . i by A24, A48, A43, A47, A32, A25, A22, Def11; :: thesis:

end;

suppose A49: not 1 + (len f) in E1 . i ; :: thesis:

then A50: ( Ee . i = E1 . i & Es . i = (E1 . i) \/ {(1 + (len f))} ) by A19, A3, Def4, Def5;

per cases by A21, A28, A25, FINSEQ_1:25;

suppose A51: s1 . i in dom f ; :: thesis:

then A52: ( ((f ^ <*d1*>) ^ <*d2*>) . s1i = f . s1i & ((f ^ <*((the_inverseOp_wrt A) . d1)*>) ^ <*d2*>) . s1i = f . s1i ) by A28, A31, FINSEQ_1:def 7;
s1i <= len f by A51, FINSEQ_3:25;
then A53: s1i < (len f) + 1 by NAT_1:13;

per cases ;

suppose A54: s1i in Ee . i ; :: thesis:

then A55: (CFe . i) . s1i = (the_inverseOp_wrt A) . (((f ^ <*d1*>) ^ <*d2*>) . s1i) by A20, A25, Def11;
s1i in Es . i by A50, A54, ZFMISC_1:136;
hence ((App CFe) . s1) . i = ((App CFs) . s2) . i by A24, A52, A55, A25, A22, Def11; :: thesis:

end;

suppose A56: not s1 . i in Ee . i ; :: thesis:

then A57: (CFe . i) . (s1 . i) = ((f ^ <*d1*>) ^ <*d2*>) . (s1 . i) by A20, A25, Def11;
not s1i in Es . i by A50, A56, A53, ZFMISC_1:136;
hence ((App CFe) . s1) . i = ((App CFs) . s2) . i by A24, A52, A57, A25, A22, Def11; :: thesis:

end;

suppose ex k being Nat st
( k in dom <*d1,d2*> & s1 . i = (len f) + k ) ; :: thesis:

then consider k being Nat such that
A58: ( k in dom <*d1,d2*> & s1 . i = (len f) + k ) ;

per cases by A58, A26, TARSKI:def 2;

suppose A59: k = 1 ; :: thesis:

then A60: (CFe . i) . s1i = d1 by A29, A49, A58, A50, A20, A25, Def11;
s1i in Es . i by A50, ZFMISC_1:136, A58, A59;
then (CFs . i) . s1i = (the_inverseOp_wrt A) . (((f ^ <*((the_inverseOp_wrt A) . d1)*>) ^ <*d2*>) . s1i) by A25, A22, Def11;
hence ((App CFe) . s1) . i = ((App CFs) . s2) . i by A24, A60, A1, A58, A59, A32, FINSEQOP:62; :: thesis:

end;

suppose A61: k = 2 ; :: thesis:

( E1 . i in rng E1 & rng E1 = F1 ) by A19, RLAFFIN3:def 1, FUNCT_1:def 3;
then E1 . i c= union F1 by ZFMISC_1:74;
then A62: E1 . i c= Seg (1 + (len f)) by A2;
1 + (len f) < (1 + (len f)) + 1 by NAT_1:13;
then A63: not s1i in E1 . i by A58, A61, A62, FINSEQ_1:1;
then A64: (CFe . i) . s1i = d2 by A29, A58, A61, A50, A20, A25, Def11;
s1i <> 1 + (len f) by A58, A61;
then not s1i in Es . i by A63, A50, ZFMISC_1:136;
hence ((App CFe) . s1) . i = ((App CFs) . s2) . i by A24, A64, A58, A61, A32, A25, A22, Def11; :: thesis:

end;

then A65: (App CFe) . s1 = (App CFs) . s2 by A17;
thus A $$ (S1,(M "**" (App CFe))) = A . ((A $$ (S11,(M "**" (App CFe)))),((M "**" (App CFe)) . s1)) by A1, A13, A14, SETWOP_2:2
.= A . ((A $$ (S22,(M "**" (App CFs)))),((M "**" (App CFs)) . s2)) by A8, A9, A15, A65, A16
.= A $$ (S2,(M "**" (App CFs))) by A1, A13, A14, SETWOP_2:2 ; :: thesis:

end;

A66: for n being Nat holds S₁[n] from NAT_1:sch 2(A5, A7);
let S1 be Element of Fin (dom (App CFe)); :: thesis:
let S2 be Element of Fin (dom (App CFs)); :: thesis:
S₁[ card S1] by A66;
hence ( S1 = S2 implies A $$ (S1,(M "**" (App CFe))) = A $$ (S2,(M "**" (App CFs))) ) ; :: thesis: