let D be non empty set ; :: thesis: for A, M being BinOp of D
for f, g being FinSequence of D
for F1 being finite set st A is having_a_unity & A is commutative & A is associative holds
for E1 being Enumeration of F1
for CE1, CE2 being non-empty non empty FinSequence of D * st CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp ((f ^ g),A,F1)) * E1 holds
for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S1 = S2 holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))
let A, M be BinOp of D; :: thesis: for f, g being FinSequence of D
for F1 being finite set st A is having_a_unity & A is commutative & A is associative holds
for E1 being Enumeration of F1
for CE1, CE2 being non-empty non empty FinSequence of D * st CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp ((f ^ g),A,F1)) * E1 holds
for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S1 = S2 holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))
let f, g be FinSequence of D; :: thesis: for F1 being finite set st A is having_a_unity & A is commutative & A is associative holds
for E1 being Enumeration of F1
for CE1, CE2 being non-empty non empty FinSequence of D * st CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp ((f ^ g),A,F1)) * E1 holds
for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S1 = S2 holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))
let F1 be finite set ; :: thesis: ( A is having_a_unity & A is commutative & A is associative implies for E1 being Enumeration of F1
for CE1, CE2 being non-empty non empty FinSequence of D * st CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp ((f ^ g),A,F1)) * E1 holds
for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S1 = S2 holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2))) )
assume A1: ( A is having_a_unity & A is commutative & A is associative ) ; :: thesis: for E1 being Enumeration of F1
for CE1, CE2 being non-empty non empty FinSequence of D * st CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp ((f ^ g),A,F1)) * E1 holds
for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S1 = S2 holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))
let E1 be Enumeration of F1; :: thesis: for CE1, CE2 being non-empty non empty FinSequence of D * st CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp ((f ^ g),A,F1)) * E1 holds
for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S1 = S2 holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))
let CE1, CE2 be non-empty non empty FinSequence of D * ; :: thesis: ( CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp ((f ^ g),A,F1)) * E1 implies for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S1 = S2 holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2))) )
assume A2: ( CE1 = (SignGenOp (f,A,F1)) * E1 & CE2 = (SignGenOp ((f ^ g),A,F1)) * E1 ) ; :: thesis: for S1 being Element of Fin (dom (App CE1))
for S2 being Element of Fin (dom (App CE2)) st S1 = S2 holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))
let S1 be Element of Fin (dom (App CE1)); :: thesis: for S2 being Element of Fin (dom (App CE2)) st S1 = S2 holds
A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))
let S2 be Element of Fin (dom (App CE2)); :: thesis: ( S1 = S2 implies A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2))) )
assume A3: S1 = S2 ; :: thesis: A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2)))
A4: ( S1 c= dom (App CE1) & dom (App CE1) = dom (M "**" (App CE1)) ) by FINSUB_1:def 5, FUNCT_2:def 1;
A5: ( S2 c= dom (App CE2) & dom (App CE2) = dom (M "**" (App CE2)) ) by FINSUB_1:def 5, FUNCT_2:def 1;
then A6: dom ((M "**" (App CE2)) | S2) = S2 by RELAT_1:62;
for x being object st x in dom ((M "**" (App CE1)) | S1) holds
((M "**" (App CE1)) | S1) . x = ((M "**" (App CE2)) | S2) . x

proof

let x be object ; :: thesis: ( x in dom ((M "**" (App CE1)) | S1) implies ((M "**" (App CE1)) | S1) . x = ((M "**" (App CE2)) | S2) . x )
assume A7: x in dom ((M "**" (App CE1)) | S1) ; :: thesis: ((M "**" (App CE1)) | S1) . x = ((M "**" (App CE2)) | S2) . x
A8: x in dom (App CE1) by A7, A4;
reconsider x = x as FinSequence by A7;
A9: x in dom (App CE2) by A7, A5, A3;
( len CE2 = len x & len x = len CE1 ) by A8, A9, Th47;
then A10: ( dom CE2 = dom x & dom x = dom CE1 ) by FINSEQ_3:30;
( len ((App CE1) . x) = len x & len x = len ((App CE2) . x) ) by A8, A9, Def9;
then A11: ( dom ((App CE1) . x) = dom x & dom x = dom ((App CE2) . x) ) by FINSEQ_3:30;
for i being Nat st i in dom ((App CE1) . x) holds
((App CE1) . x) . i = ((App CE2) . x) . i

proof

let i be Nat; :: thesis: ( i in dom ((App CE1) . x) implies ((App CE1) . x) . i = ((App CE2) . x) . i )
assume A12: i in dom ((App CE1) . x) ; :: thesis: ((App CE1) . x) . i = ((App CE2) . x) . i
(CE2 . i) . (x . i) = (CE1 . i) . (x . i)

proof

A13: ( x . i in dom (CE1 . i) & x . i in dom (CE2 . i) ) by Th47, A8, A9, A11, A12;
A14: CE1 . i = SignGen (f,A,(E1 . i)) by A2, A12, A10, A11, Th80;
A15: CE2 . i = SignGen ((f ^ g),A,(E1 . i)) by A2, A12, A10, A11, Th80;
A16: x . i in dom f by Def11, A13, A14;

per cases ( x . i in E1 . i or not x . i in E1 . i ) ;

suppose A17: x . i in E1 . i ; :: thesis: (CE2 . i) . (x . i) = (CE1 . i) . (x . i)

hence (CE2 . i) . (x . i) = (the_inverseOp_wrt A) . ((f ^ g) . (x . i)) by A15, Def11, A13
.= (the_inverseOp_wrt A) . (f . (x . i)) by A16, FINSEQ_1:def 7
.= (CE1 . i) . (x . i) by A14, Def11, A13, A17 ;
:: thesis: verum

end;

suppose A18: not x . i in E1 . i ; :: thesis: (CE2 . i) . (x . i) = (CE1 . i) . (x . i)

hence (CE2 . i) . (x . i) = (f ^ g) . (x . i) by A15, Def11, A13
.= f . (x . i) by A16, FINSEQ_1:def 7
.= (CE1 . i) . (x . i) by A14, Def11, A13, A18 ;
:: thesis: verum

end;

end;

end;

hence ((App CE1) . x) . i = (CE2 . i) . (x . i) by A12, A11, A8, Def9
.= ((App CE2) . x) . i by A12, A11, A9, Def9 ;
:: thesis: verum

end;

then A19: (App CE1) . x = (App CE2) . x by A11;
((M "**" (App CE1)) | S1) . x = (M "**" (App CE1)) . x by A7, FUNCT_1:49
.= M "**" ((App CE2) . x) by A19, A7, A4, Def10
.= (M "**" (App CE2)) . x by A7, A5, A3, Def10
.= ((M "**" (App CE2)) | S2) . x by A7, A3, FUNCT_1:49 ;
hence ((M "**" (App CE1)) | S1) . x = ((M "**" (App CE2)) | S2) . x ; :: thesis: verum

end;

then (M "**" (App CE1)) | S1 = (M "**" (App CE2)) | S2 by A3, A4, RELAT_1:62, A6;
hence A $$ (S1,(M "**" (App CE1))) = A $$ (S2,(M "**" (App CE2))) by A1, A3, Th1; :: thesis: verum