let D be non empty set ; :: thesis: for A being BinOp of D
for d, d1, d2 being Element of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F st union F c= Seg (1 + (len f)) holds
for Ee being Enumeration of Ext (F,(1 + (len f)),(2 + (len f))) st Ee = Ext (E,(1 + (len f)),(2 + (len f))) holds
for CE1, CEE being FinSequence of D * st CE1 = (SignGenOp ((f ^ <*d*>),A,F)) * E & CEE = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext (F,(1 + (len f)),(2 + (len f)))))) * Ee holds
for s being FinSequence st s in doms CE1 & rng s c= dom f holds
( s in doms CEE & (App CE1) . s = (App CEE) . s )
let A be BinOp of D; :: thesis: for d, d1, d2 being Element of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F st union F c= Seg (1 + (len f)) holds
for Ee being Enumeration of Ext (F,(1 + (len f)),(2 + (len f))) st Ee = Ext (E,(1 + (len f)),(2 + (len f))) holds
for CE1, CEE being FinSequence of D * st CE1 = (SignGenOp ((f ^ <*d*>),A,F)) * E & CEE = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext (F,(1 + (len f)),(2 + (len f)))))) * Ee holds
for s being FinSequence st s in doms CE1 & rng s c= dom f holds
( s in doms CEE & (App CE1) . s = (App CEE) . s )
let d, d1, d2 be Element of D; :: thesis: for f being FinSequence of D
for F being finite set
for E being Enumeration of F st union F c= Seg (1 + (len f)) holds
for Ee being Enumeration of Ext (F,(1 + (len f)),(2 + (len f))) st Ee = Ext (E,(1 + (len f)),(2 + (len f))) holds
for CE1, CEE being FinSequence of D * st CE1 = (SignGenOp ((f ^ <*d*>),A,F)) * E & CEE = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext (F,(1 + (len f)),(2 + (len f)))))) * Ee holds
for s being FinSequence st s in doms CE1 & rng s c= dom f holds
( s in doms CEE & (App CE1) . s = (App CEE) . s )
let f be FinSequence of D; :: thesis: for F being finite set
for E being Enumeration of F st union F c= Seg (1 + (len f)) holds
for Ee being Enumeration of Ext (F,(1 + (len f)),(2 + (len f))) st Ee = Ext (E,(1 + (len f)),(2 + (len f))) holds
for CE1, CEE being FinSequence of D * st CE1 = (SignGenOp ((f ^ <*d*>),A,F)) * E & CEE = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext (F,(1 + (len f)),(2 + (len f)))))) * Ee holds
for s being FinSequence st s in doms CE1 & rng s c= dom f holds
( s in doms CEE & (App CE1) . s = (App CEE) . s )
let F be finite set ; :: thesis: for E being Enumeration of F st union F c= Seg (1 + (len f)) holds
for Ee being Enumeration of Ext (F,(1 + (len f)),(2 + (len f))) st Ee = Ext (E,(1 + (len f)),(2 + (len f))) holds
for CE1, CEE being FinSequence of D * st CE1 = (SignGenOp ((f ^ <*d*>),A,F)) * E & CEE = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext (F,(1 + (len f)),(2 + (len f)))))) * Ee holds
for s being FinSequence st s in doms CE1 & rng s c= dom f holds
( s in doms CEE & (App CE1) . s = (App CEE) . s )
set I = the_inverseOp_wrt A;
let E be Enumeration of F; :: thesis: ( union F c= Seg (1 + (len f)) implies for Ee being Enumeration of Ext (F,(1 + (len f)),(2 + (len f))) st Ee = Ext (E,(1 + (len f)),(2 + (len f))) holds
for CE1, CEE being FinSequence of D * st CE1 = (SignGenOp ((f ^ <*d*>),A,F)) * E & CEE = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext (F,(1 + (len f)),(2 + (len f)))))) * Ee holds
for s being FinSequence st s in doms CE1 & rng s c= dom f holds
( s in doms CEE & (App CE1) . s = (App CEE) . s ) )
assume A1: union F c= Seg (1 + (len f)) ; :: thesis: for Ee being Enumeration of Ext (F,(1 + (len f)),(2 + (len f))) st Ee = Ext (E,(1 + (len f)),(2 + (len f))) holds
for CE1, CEE being FinSequence of D * st CE1 = (SignGenOp ((f ^ <*d*>),A,F)) * E & CEE = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext (F,(1 + (len f)),(2 + (len f)))))) * Ee holds
for s being FinSequence st s in doms CE1 & rng s c= dom f holds
( s in doms CEE & (App CE1) . s = (App CEE) . s )
set EF = Ext (F,(1 + (len f)),(2 + (len f)));
let Ee be Enumeration of Ext (F,(1 + (len f)),(2 + (len f))); :: thesis: ( Ee = Ext (E,(1 + (len f)),(2 + (len f))) implies for CE1, CEE being FinSequence of D * st CE1 = (SignGenOp ((f ^ <*d*>),A,F)) * E & CEE = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext (F,(1 + (len f)),(2 + (len f)))))) * Ee holds
for s being FinSequence st s in doms CE1 & rng s c= dom f holds
( s in doms CEE & (App CE1) . s = (App CEE) . s ) )
assume A2: Ee = Ext (E,(1 + (len f)),(2 + (len f))) ; :: thesis: for CE1, CEE being FinSequence of D * st CE1 = (SignGenOp ((f ^ <*d*>),A,F)) * E & CEE = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext (F,(1 + (len f)),(2 + (len f)))))) * Ee holds
for s being FinSequence st s in doms CE1 & rng s c= dom f holds
( s in doms CEE & (App CE1) . s = (App CEE) . s )
let CE1, CEE be FinSequence of D * ; :: thesis: ( CE1 = (SignGenOp ((f ^ <*d*>),A,F)) * E & CEE = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext (F,(1 + (len f)),(2 + (len f)))))) * Ee implies for s being FinSequence st s in doms CE1 & rng s c= dom f holds
( s in doms CEE & (App CE1) . s = (App CEE) . s ) )
assume A3: ( CE1 = (SignGenOp ((f ^ <*d*>),A,F)) * E & CEE = (SignGenOp (((f ^ <*d1*>) ^ <*d2*>),A,(Ext (F,(1 + (len f)),(2 + (len f)))))) * Ee ) ; :: thesis: for s being FinSequence st s in doms CE1 & rng s c= dom f holds
( s in doms CEE & (App CE1) . s = (App CEE) . s )
let s be FinSequence; :: thesis: ( s in doms CE1 & rng s c= dom f implies ( s in doms CEE & (App CE1) . s = (App CEE) . s ) )
assume A4: ( s in doms CE1 & rng s c= dom f ) ; :: thesis: ( s in doms CEE & (App CE1) . s = (App CEE) . s )
A5: 1 + (len f) < (1 + (len f)) + 1 by NAT_1:13;
then A6: not 2 + (len f) in union F by A1, FINSEQ_1:1;
A7: len ((f ^ <*d1*>) ^ <*d2*>) = (len (f ^ <*d1*>)) + 1 by FINSEQ_2:16
.= ((len f) + 1) + 1 by FINSEQ_2:16 ;
len (f ^ <*d*>) = (len f) + 1 by FINSEQ_2:16;
then A8: doms CE1 c= doms CEE by A3, A5, A6, A7, Th10, Th107;
hence s in doms CEE by A4; :: thesis: (App CE1) . s = (App CEE) . s
A9: ( len E = len CE1 & len CE1 = len s & len s = len CEE ) by A3, A8, Th47, A4, CARD_1:def 7;
A10: ( len ((App CEE) . s) = len s & len s = len ((App CE1) . s) ) by A8, A4, Def9;
for i being Nat st 1 <= i & i <= len s holds
((App CE1) . s) . i = ((App CEE) . s) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len s implies ((App CE1) . s) . i = ((App CEE) . s) . i )
assume A11: ( 1 <= i & i <= len s ) ; :: thesis: ((App CE1) . s) . i = ((App CEE) . s) . i
reconsider si = s . i as Nat by A4;
A12: ( i in dom CE1 & i in dom CEE & i in dom E & i in dom s ) by A11, A9, FINSEQ_3:25;
then A13: ( ((App CE1) . s) . i = (CE1 . i) . si & CE1 . i = SignGen ((f ^ <*d*>),A,(E . i)) & ((App CEE) . s) . i = (CEE . i) . si & CEE . i = SignGen (((f ^ <*d1*>) ^ <*d2*>),A,(Ee . i)) ) by A3, A4, A8, Def9, Th80;
A14: si in rng s by A12, FUNCT_1:def 3;
then A15: ( si <= len f & len f < (len f) + 2 ) by A4, FINSEQ_3:25, NAT_1:16;
dom f c= dom (f ^ <*d*>) by FINSEQ_1:26;
then si in dom (f ^ <*d*>) by A14, A4;
then A16: si in dom (SignGen ((f ^ <*d*>),A,(E . i))) by Def11;
A17: (f ^ <*d1*>) ^ <*d2*> = f ^ <*d1,d2*> by FINSEQ_1:32;
dom f c= dom (f ^ <*d1,d2*>) by FINSEQ_1:26;
then si in dom ((f ^ <*d1*>) ^ <*d2*>) by A14, A4, A17;
then A18: si in dom (SignGen (((f ^ <*d1*>) ^ <*d2*>),A,(Ee . i))) by Def11;

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

suppose A19: si in E . i ; :: thesis: ((App CE1) . s) . i = ((App CEE) . s) . i

then A20: (SignGen ((f ^ <*d*>),A,(E . i))) . si = (the_inverseOp_wrt A) . ((f ^ <*d*>) . si) by A16, Def11
.= (the_inverseOp_wrt A) . (f . si) by A14, A4, FINSEQ_1:def 7 ;

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

suppose 1 + (len f) in E . i ; :: thesis: ((App CE1) . s) . i = ((App CEE) . s) . i

then Ee . i = (E . i) \/ {(2 + (len f))} by A2, A12, Def5;
then si in Ee . i by A19, ZFMISC_1:136;
then (SignGen (((f ^ <*d1*>) ^ <*d2*>),A,(Ee . i))) . si = (the_inverseOp_wrt A) . ((f ^ <*d1,d2*>) . si) by A17, A18, Def11
.= (the_inverseOp_wrt A) . (f . si) by A14, A4, FINSEQ_1:def 7 ;
hence ((App CE1) . s) . i = ((App CEE) . s) . i by A20, A13; :: thesis: verum

end;

suppose not 1 + (len f) in E . i ; :: thesis: ((App CE1) . s) . i = ((App CEE) . s) . i

then si in Ee . i by A19, A2, A12, Def5;
then (SignGen (((f ^ <*d1*>) ^ <*d2*>),A,(Ee . i))) . si = (the_inverseOp_wrt A) . ((f ^ <*d1,d2*>) . si) by A17, A18, Def11
.= (the_inverseOp_wrt A) . (f . si) by A14, A4, FINSEQ_1:def 7 ;
hence ((App CE1) . s) . i = ((App CEE) . s) . i by A20, A13; :: thesis: verum

end;

end;

end;

suppose A21: not si in E . i ; :: thesis: ((App CE1) . s) . i = ((App CEE) . s) . i

then A22: (SignGen ((f ^ <*d*>),A,(E . i))) . si = (f ^ <*d*>) . si by A16, Def11
.= f . si by A14, A4, FINSEQ_1:def 7 ;

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

suppose 1 + (len f) in E . i ; :: thesis: ((App CE1) . s) . i = ((App CEE) . s) . i

then Ee . i = (E . i) \/ {(2 + (len f))} by A2, A12, Def5;
then not si in Ee . i by A15, A21, ZFMISC_1:136;
then (SignGen (((f ^ <*d1*>) ^ <*d2*>),A,(Ee . i))) . si = (f ^ <*d1,d2*>) . si by A17, A18, Def11
.= f . si by A14, A4, FINSEQ_1:def 7 ;
hence ((App CE1) . s) . i = ((App CEE) . s) . i by A22, A13; :: thesis: verum

end;

suppose not 1 + (len f) in E . i ; :: thesis: ((App CE1) . s) . i = ((App CEE) . s) . i

then not si in Ee . i by A21, A2, A12, Def5;
then (SignGen (((f ^ <*d1*>) ^ <*d2*>),A,(Ee . i))) . si = (f ^ <*d1,d2*>) . si by A17, A18, Def11
.= f . si by A14, A4, FINSEQ_1:def 7 ;
hence ((App CE1) . s) . i = ((App CEE) . s) . i by A22, A13; :: thesis: verum

end;

end;

end;

end;

end;

hence (App CE1) . s = (App CEE) . s by A10; :: thesis: verum