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 | (union F1) is one-to-one holds
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st 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
g * s in doms ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)
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 | (union F1) is one-to-one holds
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st 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
g * s in doms ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)
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 | (union F1) is one-to-one holds
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st 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
g * s in doms ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)
let F1 be finite set ; :: thesis: for E1 being Enumeration of F1
for g being Function st union F1 c= dom g & g | (union F1) is one-to-one holds
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st 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
g * s in doms ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)
let E1 be Enumeration of F1; :: thesis: for g being Function st union F1 c= dom g & g | (union F1) is one-to-one holds
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st 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
g * s in doms ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)
let g be Function; :: thesis: ( union F1 c= dom g & g | (union F1) is one-to-one implies for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st 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
g * s in doms ((SignGenOp (fg,A,((.: g) .: F1))) * gE1) )
assume A1: ( union F1 c= dom g & g | (union F1) is one-to-one ) ; :: thesis: for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st 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
g * s in doms ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)
let gE1 be Enumeration of (.: g) .: F1; :: thesis: ( gE1 = (.: g) * E1 implies for fg being FinSequence of D st 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
g * s in doms ((SignGenOp (fg,A,((.: g) .: F1))) * gE1) )
assume A2: gE1 = (.: g) * E1 ; :: thesis: for fg being FinSequence of D st 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
g * s in doms ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)
A3: ( 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: ( 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
g * s in doms ((SignGenOp (gf,A,((.: g) .: F1))) * gE1) )
assume A4: 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
g * s in doms ((SignGenOp (gf,A,((.: g) .: F1))) * gE1)
let s be FinSequence; :: thesis: ( s in doms ((SignGenOp (f,A,F1)) * E1) & rng s c= dom g implies g * s in doms ((SignGenOp (gf,A,((.: g) .: F1))) * gE1) )
assume that
A5: s in doms ((SignGenOp (f,A,F1)) * E1) and
A6: rng s c= dom g ; :: thesis: g * s in doms ((SignGenOp (gf,A,((.: g) .: F1))) * gE1)
A7: ( dom (g * s) = dom s & dom s = Seg (len s) ) by A6, RELAT_1:27, FINSEQ_1:def 3;
then reconsider gs = g * s as FinSequence by FINSEQ_1:def 2;
A8: len s = len ((SignGenOp (f,A,F1)) * E1) by A5, Th47;
then A9: dom s = dom ((SignGenOp (f,A,F1)) * E1) by FINSEQ_3:30;
( dom (SignGenOp (gf,A,((.: g) .: F1))) = (.: g) .: F1 & (.: g) .: F1 = rng gE1 ) by FUNCT_2:def 1, RLAFFIN3:def 1;
then A10: dom ((SignGenOp (gf,A,((.: g) .: F1))) * gE1) = dom gE1 by RELAT_1:27;
( F1 c= bool (union F1) & bool (union F1) c= bool (dom g) ) by A1, ZFMISC_1:67, ZFMISC_1:82;
then F1 c= bool (dom g) ;
then F1 c= dom (.: g) by FUNCT_3:def 1;
then rng E1 c= dom (.: g) ;
then A11: dom gE1 = dom E1 by A2, RELAT_1:27;
len gs = len s by A7, FINSEQ_3:29;
then A12: len gs = len ((SignGenOp (gf,A,((.: g) .: F1))) * gE1) by A3, A8, A10, FINSEQ_3:29;
for i being Nat st i in dom gs holds
gs . i in dom (((SignGenOp (gf,A,((.: g) .: F1))) * gE1) . i)

proof

let i be Nat; :: thesis: ( i in dom gs implies gs . i in dom (((SignGenOp (gf,A,((.: g) .: F1))) * gE1) . i) )
assume A13: i in dom gs ; :: thesis: gs . i in dom (((SignGenOp (gf,A,((.: g) .: F1))) * gE1) . i)
A14: ( i in dom s & s . i in dom g ) by A13, FUNCT_1:11;
then A15: s . i in dom (((SignGenOp (f,A,F1)) * E1) . i) by Th47, A5;
s . i in dom (SignGen (f,A,(E1 . i))) by A15, Th80, A9, A14;
then A16: s . i in dom f by Def11;
i in dom E1 by A9, A14, FUNCT_1:11;
then A17: ((SignGenOp (gf,A,((.: g) .: F1))) * gE1) . i = SignGen (gf,A,(gE1 . i)) by Th80, A11;
A18: dom (SignGen (gf,A,(gE1 . i))) = dom gf by Def11;
A19: ( gs . i = g . (s . i) & i in dom gs ) by A14, FUNCT_1:11, FUNCT_1:13;
s . i in dom g by A13, FUNCT_1:11;
then g . (s . i) in g .: (dom f) by A16, FUNCT_1:def 6;
hence gs . i in dom (((SignGenOp (gf,A,((.: g) .: F1))) * gE1) . i) by A17, A18, A4, A19; :: thesis: verum

end;

hence g * s in doms ((SignGenOp (gf,A,((.: g) .: F1))) * gE1) by A12, Th47; :: thesis: verum