let D be non empty set ; :: thesis: for A being BinOp of D
for d1, d2 being Element of D
for f being FinSequence of D
for F1 being finite set
for E1 being Enumeration of F1
for CE1, CE2 being D * -valued FinSequence st CE1 = (SignGenOp ((f ^ <*d1*>),A,F1)) * E1 & CE2 = (SignGenOp ((f ^ <*d2*>),A,F1)) * E1 holds
for s being FinSequence st s in doms CE1 & not 1 + (len f) in rng s holds
( s in doms CE2 & (App CE1) . s = (App CE2) . s )
let A be BinOp of D; :: thesis: for d1, d2 being Element of D
for f being FinSequence of D
for F1 being finite set
for E1 being Enumeration of F1
for CE1, CE2 being D * -valued FinSequence st CE1 = (SignGenOp ((f ^ <*d1*>),A,F1)) * E1 & CE2 = (SignGenOp ((f ^ <*d2*>),A,F1)) * E1 holds
for s being FinSequence st s in doms CE1 & not 1 + (len f) in rng s holds
( s in doms CE2 & (App CE1) . s = (App CE2) . s )
let d1, d2 be Element of D; :: thesis: for f being FinSequence of D
for F1 being finite set
for E1 being Enumeration of F1
for CE1, CE2 being D * -valued FinSequence st CE1 = (SignGenOp ((f ^ <*d1*>),A,F1)) * E1 & CE2 = (SignGenOp ((f ^ <*d2*>),A,F1)) * E1 holds
for s being FinSequence st s in doms CE1 & not 1 + (len f) in rng s holds
( s in doms CE2 & (App CE1) . s = (App CE2) . s )
let f be FinSequence of D; :: thesis: for F1 being finite set
for E1 being Enumeration of F1
for CE1, CE2 being D * -valued FinSequence st CE1 = (SignGenOp ((f ^ <*d1*>),A,F1)) * E1 & CE2 = (SignGenOp ((f ^ <*d2*>),A,F1)) * E1 holds
for s being FinSequence st s in doms CE1 & not 1 + (len f) in rng s holds
( s in doms CE2 & (App CE1) . s = (App CE2) . s )
let F1 be finite set ; :: thesis: for E1 being Enumeration of F1
for CE1, CE2 being D * -valued FinSequence st CE1 = (SignGenOp ((f ^ <*d1*>),A,F1)) * E1 & CE2 = (SignGenOp ((f ^ <*d2*>),A,F1)) * E1 holds
for s being FinSequence st s in doms CE1 & not 1 + (len f) in rng s holds
( s in doms CE2 & (App CE1) . s = (App CE2) . s )
set I = the_inverseOp_wrt A;
let E1 be Enumeration of F1; :: thesis: for CE1, CE2 being D * -valued FinSequence st CE1 = (SignGenOp ((f ^ <*d1*>),A,F1)) * E1 & CE2 = (SignGenOp ((f ^ <*d2*>),A,F1)) * E1 holds
for s being FinSequence st s in doms CE1 & not 1 + (len f) in rng s holds
( s in doms CE2 & (App CE1) . s = (App CE2) . s )
let CE1, CE2 be D * -valued FinSequence; :: thesis: ( CE1 = (SignGenOp ((f ^ <*d1*>),A,F1)) * E1 & CE2 = (SignGenOp ((f ^ <*d2*>),A,F1)) * E1 implies for s being FinSequence st s in doms CE1 & not 1 + (len f) in rng s holds
( s in doms CE2 & (App CE1) . s = (App CE2) . s ) )
assume A1: ( CE1 = (SignGenOp ((f ^ <*d1*>),A,F1)) * E1 & CE2 = (SignGenOp ((f ^ <*d2*>),A,F1)) * E1 ) ; :: thesis: for s being FinSequence st s in doms CE1 & not 1 + (len f) in rng s holds
( s in doms CE2 & (App CE1) . s = (App CE2) . s )
let s be FinSequence; :: thesis: ( s in doms CE1 & not 1 + (len f) in rng s implies ( s in doms CE2 & (App CE1) . s = (App CE2) . s ) )
assume A2: ( s in doms CE1 & not 1 + (len f) in rng s ) ; :: thesis: ( s in doms CE2 & (App CE1) . s = (App CE2) . s )
A3: len (f ^ <*d1*>) = (len f) + 1 by FINSEQ_2:16;
len (f ^ <*d2*>) = (len f) + 1 by FINSEQ_2:16;
then A4: doms CE1 c= doms CE2 by A1, A3, Th107;
hence s in doms CE2 by A2; :: thesis: (App CE1) . s = (App CE2) . s
A5: ( len CE1 = len s & len s = len CE2 ) by A4, Th47, A2;
A6: ( len ((App CE2) . s) = len s & len s = len ((App CE1) . s) ) by A4, A2, Def9;
for i being Nat st 1 <= i & i <= len s holds
((App CE1) . s) . i = ((App CE2) . s) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len s implies ((App CE1) . s) . i = ((App CE2) . s) . i )
assume A7: ( 1 <= i & i <= len s ) ; :: thesis: ((App CE1) . s) . i = ((App CE2) . s) . i
reconsider si = s . i as Nat by A2;
A8: ( i in dom CE1 & i in dom CE2 & i in dom s ) by A7, A5, FINSEQ_3:25;
then A9: ( ((App CE1) . s) . i = (CE1 . i) . si & CE1 . i = SignGen ((f ^ <*d1*>),A,(E1 . i)) & ((App CE2) . s) . i = (CE2 . i) . si & CE2 . i = SignGen ((f ^ <*d2*>),A,(E1 . i)) ) by A1, A2, A4, Def9, Th80;
A10: si <> 1 + (len f) by A2, A8, FUNCT_1:def 3;
si in dom (CE1 . i) by A2, A8, Th47;
then si in dom (f ^ <*d1*>) by A9, Def11;
then A11: ( 1 <= si & si <= (len f) + 1 ) by A3, FINSEQ_3:25;
then si < (len f) + 1 by A10, XXREAL_0:1;
then A12: si <= len f by NAT_1:13;
then A13: si in dom f by A11, FINSEQ_3:25;
( dom f c= dom (f ^ <*d1*>) & dom f c= dom (f ^ <*d2*>) ) by FINSEQ_1:26;
then ( si in dom (f ^ <*d1*>) & si in dom (f ^ <*d2*>) ) by A12, A11, FINSEQ_3:25;
then A14: ( si in dom (SignGen ((f ^ <*d1*>),A,(E1 . i))) & si in dom (SignGen ((f ^ <*d2*>),A,(E1 . i))) ) by Def11;

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

suppose A15: si in E1 . i ; :: thesis: ((App CE1) . s) . i = ((App CE2) . s) . i

then A16: (SignGen ((f ^ <*d1*>),A,(E1 . i))) . si = (the_inverseOp_wrt A) . ((f ^ <*d1*>) . si) by A14, Def11
.= (the_inverseOp_wrt A) . (f . si) by A13, FINSEQ_1:def 7 ;
(SignGen ((f ^ <*d2*>),A,(E1 . i))) . si = (the_inverseOp_wrt A) . ((f ^ <*d2*>) . si) by A15, A14, Def11
.= (the_inverseOp_wrt A) . (f . si) by A13, FINSEQ_1:def 7 ;
hence ((App CE1) . s) . i = ((App CE2) . s) . i by A16, A9; :: thesis: verum

end;

suppose A17: not si in E1 . i ; :: thesis: ((App CE1) . s) . i = ((App CE2) . s) . i

then A18: (SignGen ((f ^ <*d1*>),A,(E1 . i))) . si = (f ^ <*d1*>) . si by A14, Def11
.= f . si by A13, FINSEQ_1:def 7 ;
(SignGen ((f ^ <*d2*>),A,(E1 . i))) . si = (f ^ <*d2*>) . si by A17, A14, Def11
.= f . si by A13, FINSEQ_1:def 7 ;
hence ((App CE1) . s) . i = ((App CE2) . s) . i by A18, A9; :: thesis: verum

end;

end;

end;

hence (App CE1) . s = (App CE2) . s by A6; :: thesis: verum