let D be non empty set ; :: thesis: for A being BinOp of D
for f being FinSequence of D
for F1 being finite set
for E1 being Enumeration of F1
for g being Function st union F1 c= dom g & g is one-to-one holds
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = (f * (g ")) | (dom fg) & g .: (dom f) c= dom fg holds
for s being FinSequence st s in doms ((SignGenOp (f,A,F1)) * E1) & rng s c= dom g holds
(App ((SignGenOp (f,A,F1)) * E1)) . s = (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)) . (g * s)
let A be BinOp of D; :: thesis: for f being FinSequence of D
for F1 being finite set
for E1 being Enumeration of F1
for g being Function st union F1 c= dom g & g is one-to-one holds
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = (f * (g ")) | (dom fg) & g .: (dom f) c= dom fg holds
for s being FinSequence st s in doms ((SignGenOp (f,A,F1)) * E1) & rng s c= dom g holds
(App ((SignGenOp (f,A,F1)) * E1)) . s = (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)) . (g * s)
let f be FinSequence of D; :: thesis: for F1 being finite set
for E1 being Enumeration of F1
for g being Function st union F1 c= dom g & g is one-to-one holds
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = (f * (g ")) | (dom fg) & g .: (dom f) c= dom fg holds
for s being FinSequence st s in doms ((SignGenOp (f,A,F1)) * E1) & rng s c= dom g holds
(App ((SignGenOp (f,A,F1)) * E1)) . s = (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)) . (g * s)
let F1 be finite set ; :: thesis: for E1 being Enumeration of F1
for g being Function st union F1 c= dom g & g is one-to-one holds
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = (f * (g ")) | (dom fg) & g .: (dom f) c= dom fg holds
for s being FinSequence st s in doms ((SignGenOp (f,A,F1)) * E1) & rng s c= dom g holds
(App ((SignGenOp (f,A,F1)) * E1)) . s = (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)) . (g * s)
let E1 be Enumeration of F1; :: thesis: for g being Function st union F1 c= dom g & g is one-to-one holds
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = (f * (g ")) | (dom fg) & g .: (dom f) c= dom fg holds
for s being FinSequence st s in doms ((SignGenOp (f,A,F1)) * E1) & rng s c= dom g holds
(App ((SignGenOp (f,A,F1)) * E1)) . s = (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)) . (g * s)
let g be Function; :: thesis: ( union F1 c= dom g & g is one-to-one implies for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = (f * (g ")) | (dom fg) & g .: (dom f) c= dom fg holds
for s being FinSequence st s in doms ((SignGenOp (f,A,F1)) * E1) & rng s c= dom g holds
(App ((SignGenOp (f,A,F1)) * E1)) . s = (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)) . (g * s) )
assume A1: ( union F1 c= dom g & g is one-to-one ) ; :: thesis: for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = (f * (g ")) | (dom fg) & g .: (dom f) c= dom fg holds
for s being FinSequence st s in doms ((SignGenOp (f,A,F1)) * E1) & rng s c= dom g holds
(App ((SignGenOp (f,A,F1)) * E1)) . s = (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)) . (g * s)
let gE1 be Enumeration of (.: g) .: F1; :: thesis: ( gE1 = (.: g) * E1 implies for fg being FinSequence of D st fg = (f * (g ")) | (dom fg) & g .: (dom f) c= dom fg holds
for s being FinSequence st s in doms ((SignGenOp (f,A,F1)) * E1) & rng s c= dom g holds
(App ((SignGenOp (f,A,F1)) * E1)) . s = (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)) . (g * s) )
assume A2: gE1 = (.: g) * E1 ; :: thesis: for fg being FinSequence of D st fg = (f * (g ")) | (dom fg) & g .: (dom f) c= dom fg holds
for s being FinSequence st s in doms ((SignGenOp (f,A,F1)) * E1) & rng s c= dom g holds
(App ((SignGenOp (f,A,F1)) * E1)) . s = (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)) . (g * s)
A3: g | (union F1) is one-to-one by A1, FUNCT_1:52;
then A4: ( len ((SignGenOp (f,A,F1)) * E1) = len E1 & len E1 = len gE1 & len gE1 = len ((SignGenOp (f,A,((.: g) .: F1))) * gE1) ) by A1, A2, Th97, CARD_1:def 7;
let gf be FinSequence of D; :: thesis: ( gf = (f * (g ")) | (dom gf) & g .: (dom f) c= dom gf implies for s being FinSequence st s in doms ((SignGenOp (f,A,F1)) * E1) & rng s c= dom g holds
(App ((SignGenOp (f,A,F1)) * E1)) . s = (App ((SignGenOp (gf,A,((.: g) .: F1))) * gE1)) . (g * s) )
assume that
A5: gf = (f * (g ")) | (dom gf) and
A6: g .: (dom f) c= dom gf ; :: thesis: for s being FinSequence st s in doms ((SignGenOp (f,A,F1)) * E1) & rng s c= dom g holds
(App ((SignGenOp (f,A,F1)) * E1)) . s = (App ((SignGenOp (gf,A,((.: g) .: F1))) * gE1)) . (g * s)
let s be FinSequence; :: thesis: ( s in doms ((SignGenOp (f,A,F1)) * E1) & rng s c= dom g implies (App ((SignGenOp (f,A,F1)) * E1)) . s = (App ((SignGenOp (gf,A,((.: g) .: F1))) * gE1)) . (g * s) )
assume that
A7: s in doms ((SignGenOp (f,A,F1)) * E1) and
A8: rng s c= dom g ; :: thesis: (App ((SignGenOp (f,A,F1)) * E1)) . s = (App ((SignGenOp (gf,A,((.: g) .: F1))) * gE1)) . (g * s)
( dom (g * s) = dom s & dom s = Seg (len s) ) by A8, RELAT_1:27, FINSEQ_1:def 3;
then reconsider gs = g * s as FinSequence by FINSEQ_1:def 2;
A9: ( dom (g * s) = dom s & dom s = Seg (len s) ) by A8, RELAT_1:27, FINSEQ_1:def 3;
then reconsider gs = g * s as FinSequence by FINSEQ_1:def 2;
A10: ( len gs = len s & len s = len ((SignGenOp (f,A,((.: g) .: F1))) * gE1) ) by A9, FINSEQ_3:29, Th47, A4, A7;
A11: gs in doms ((SignGenOp (gf,A,((.: g) .: F1))) * gE1) by A2, A1, A3, A6, Th98, A8, A7;
len s = len ((SignGenOp (f,A,F1)) * E1) by A7, Th47;
then A12: dom s = dom ((SignGenOp (f,A,F1)) * E1) by FINSEQ_3:30;
A13: ( gs = g * s & gs in doms ((SignGenOp (gf,A,((.: g) .: F1))) * gE1) ) by A2, A1, A3, A6, Th98, A8, A7;
A14: len ((App ((SignGenOp (f,A,F1)) * E1)) . s) = len s by Def9, A7;
for i being Nat st 1 <= i & i <= len s holds
((App ((SignGenOp (f,A,F1)) * E1)) . s) . i = ((App ((SignGenOp (gf,A,((.: g) .: F1))) * gE1)) . gs) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len s implies ((App ((SignGenOp (f,A,F1)) * E1)) . s) . i = ((App ((SignGenOp (gf,A,((.: g) .: F1))) * gE1)) . gs) . i )
assume A15: ( 1 <= i & i <= len s ) ; :: thesis: ((App ((SignGenOp (f,A,F1)) * E1)) . s) . i = ((App ((SignGenOp (gf,A,((.: g) .: F1))) * gE1)) . gs) . i
A16: i in dom s by A15, FINSEQ_3:25;
A17: s . i in rng s by A16, FUNCT_1:def 3;
A18: ( gs . i = g . (s . i) & i in dom gs ) by A17, A8, A16, FUNCT_1:11, FUNCT_1:13;
len gs = len ((SignGenOp (gf,A,((.: g) .: F1))) * gE1) by A13, Th47;
then A19: dom gs = dom ((SignGenOp (gf,A,((.: g) .: F1))) * gE1) by FINSEQ_3:30;
then A20: ((SignGenOp (gf,A,((.: g) .: F1))) * gE1) . i = SignGen (gf,A,(gE1 . i)) by A17, A8, A16, FUNCT_1:11, Th80;
A21: ((SignGenOp (f,A,F1)) * E1) . i = SignGen (f,A,(E1 . i)) by A15, FINSEQ_3:25, A12, Th80;
A22: i in dom gs by A17, A8, A16, FUNCT_1:11;
A23: ((App ((SignGenOp (f,A,F1)) * E1)) . s) . i = (((SignGenOp (f,A,F1)) * E1) . i) . (s . i) by A7, A16, Def9
.= (SignGen (f,A,(E1 . i))) . (s . i) by A15, FINSEQ_3:25, A12, Th80 ;
A24: ((App ((SignGenOp (gf,A,((.: g) .: F1))) * gE1)) . gs) . i = (((SignGenOp (gf,A,((.: g) .: F1))) * gE1) . i) . (gs . i) by A17, A8, A16, FUNCT_1:11, Def9, A13
.= (SignGen (gf,A,(gE1 . i))) . (gs . i) by A19, A17, A8, A16, FUNCT_1:11, Th80 ;
A25: s . i in dom (SignGen (f,A,(E1 . i))) by A21, A7, A16, Th47;
A26: gs . i in dom (SignGen (gf,A,(gE1 . i))) by A20, A22, A13, Th47;
A27: dom (SignGen (gf,A,(gE1 . i))) = dom gf by Def11;
A28: i in dom E1 by A12, A16, FUNCT_1:11;
then ( E1 . i in rng E1 & rng E1 = F1 ) by RLAFFIN3:def 1, FUNCT_1:def 3;
then E1 . i c= union F1 by ZFMISC_1:74;
then A29: E1 . i c= dom g by A1;
then E1 . i in bool (dom g) ;
then A30: E1 . i in dom (.: g) by FUNCT_3:def 1;
gE1 . i = (.: g) . (E1 . i) by A28, A2, A30, FUNCT_1:11, FUNCT_1:12;
then A31: gE1 . i = g .: (E1 . i) by A29, FUNCT_3:def 1;
( gs . i in dom (f * (g ")) & gf . (gs . i) = (f * (g ")) . (gs . i) ) by A26, A27, FUNCT_1:47, RELAT_1:57, A5;
then A32: gf . (gs . i) = f . ((g ") . (gs . i)) by FUNCT_1:12
.= f . (s . i) by A1, A17, A8, A18, FUNCT_1:34 ;

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

suppose A33: s . i in E1 . i ; :: thesis: ((App ((SignGenOp (f,A,F1)) * E1)) . s) . i = ((App ((SignGenOp (gf,A,((.: g) .: F1))) * gE1)) . gs) . i

then A34: (SignGen (f,A,(E1 . i))) . (s . i) = (the_inverseOp_wrt A) . (f . (s . i)) by A25, Def11;
gs . i in gE1 . i by A31, A17, A8, A33, A18, FUNCT_1:def 6;
hence ((App ((SignGenOp (f,A,F1)) * E1)) . s) . i = ((App ((SignGenOp (gf,A,((.: g) .: F1))) * gE1)) . gs) . i by A23, A24, A34, A32, A26, Def11; :: thesis: verum

end;

suppose A35: not s . i in E1 . i ; :: thesis: ((App ((SignGenOp (f,A,F1)) * E1)) . s) . i = ((App ((SignGenOp (gf,A,((.: g) .: F1))) * gE1)) . gs) . i

then A36: (SignGen (f,A,(E1 . i))) . (s . i) = f . (s . i) by A25, Def11;
not gs . i in gE1 . i

proof

assume gs . i in gE1 . i ; :: thesis: contradiction
then ex x being object st
( x in dom g & x in E1 . i & gs . i = g . x ) by A31, FUNCT_1:def 6;
hence contradiction by A35, A17, A8, A18, A1; :: thesis: verum

end;

hence ((App ((SignGenOp (f,A,F1)) * E1)) . s) . i = ((App ((SignGenOp (gf,A,((.: g) .: F1))) * gE1)) . gs) . i by A23, A24, A36, A32, A26, Def11; :: thesis: verum

end;

end;

end;

hence (App ((SignGenOp (f,A,F1)) * E1)) . s = (App ((SignGenOp (gf,A,((.: g) .: F1))) * gE1)) . (g * s) by A10, Def9, A11, A14; :: thesis: verum