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 st union F1 c= dom f holds
for g being Permutation of (dom f)
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = f * (g ") holds
for S1 being Element of Fin (dom (App ((SignGenOp (f,A,F1)) * E1))) holds { (g * s) where s is FinSequence of NAT : s in S1 } is Element of Fin (dom (App ((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 st union F1 c= dom f holds
for g being Permutation of (dom f)
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = f * (g ") holds
for S1 being Element of Fin (dom (App ((SignGenOp (f,A,F1)) * E1))) holds { (g * s) where s is FinSequence of NAT : s in S1 } is Element of Fin (dom (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)))
let f be FinSequence of D; :: thesis: for F1 being finite set
for E1 being Enumeration of F1 st union F1 c= dom f holds
for g being Permutation of (dom f)
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = f * (g ") holds
for S1 being Element of Fin (dom (App ((SignGenOp (f,A,F1)) * E1))) holds { (g * s) where s is FinSequence of NAT : s in S1 } is Element of Fin (dom (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)))
let F1 be finite set ; :: thesis: for E1 being Enumeration of F1 st union F1 c= dom f holds
for g being Permutation of (dom f)
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = f * (g ") holds
for S1 being Element of Fin (dom (App ((SignGenOp (f,A,F1)) * E1))) holds { (g * s) where s is FinSequence of NAT : s in S1 } is Element of Fin (dom (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)))
let E1 be Enumeration of F1; :: thesis: ( union F1 c= dom f implies for g being Permutation of (dom f)
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = f * (g ") holds
for S1 being Element of Fin (dom (App ((SignGenOp (f,A,F1)) * E1))) holds { (g * s) where s is FinSequence of NAT : s in S1 } is Element of Fin (dom (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1))) )
assume A1: union F1 c= dom f ; :: thesis: for g being Permutation of (dom f)
for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = f * (g ") holds
for S1 being Element of Fin (dom (App ((SignGenOp (f,A,F1)) * E1))) holds { (g * s) where s is FinSequence of NAT : s in S1 } is Element of Fin (dom (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)))
let g be Permutation of (dom f); :: thesis: for gE1 being Enumeration of (.: g) .: F1 st gE1 = (.: g) * E1 holds
for fg being FinSequence of D st fg = f * (g ") holds
for S1 being Element of Fin (dom (App ((SignGenOp (f,A,F1)) * E1))) holds { (g * s) where s is FinSequence of NAT : s in S1 } is Element of Fin (dom (App ((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 fg = f * (g ") holds
for S1 being Element of Fin (dom (App ((SignGenOp (f,A,F1)) * E1))) holds { (g * s) where s is FinSequence of NAT : s in S1 } is Element of Fin (dom (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1))) )
assume A2: gE1 = (.: g) * E1 ; :: thesis: for fg being FinSequence of D st fg = f * (g ") holds
for S1 being Element of Fin (dom (App ((SignGenOp (f,A,F1)) * E1))) holds { (g * s) where s is FinSequence of NAT : s in S1 } is Element of Fin (dom (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)))
let fg be FinSequence of D; :: thesis: ( fg = f * (g ") implies for S1 being Element of Fin (dom (App ((SignGenOp (f,A,F1)) * E1))) holds { (g * s) where s is FinSequence of NAT : s in S1 } is Element of Fin (dom (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1))) )
assume A3: fg = f * (g ") ; :: thesis: for S1 being Element of Fin (dom (App ((SignGenOp (f,A,F1)) * E1))) holds { (g * s) where s is FinSequence of NAT : s in S1 } is Element of Fin (dom (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)))
let S1 be Element of Fin (dom (App ((SignGenOp (f,A,F1)) * E1))); :: thesis: { (g * s) where s is FinSequence of NAT : s in S1 } is Element of Fin (dom (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)))
A4: union F1 c= dom g by A1, FUNCT_2:52;
A5: g | (union F1) is one-to-one by FUNCT_1:52;
( dom (g ") = dom f & dom f = rng (g ") ) by FUNCT_2:52, FUNCT_2:def 3;
then A6: dom (f * (g ")) = dom f by RELAT_1:27;
A7: g .: (dom f) c= dom fg by A6, A3;
{ (g * s) where s is FinSequence of NAT : s in S1 } c= dom (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { (g * s) where s is FinSequence of NAT : s in S1 } or y in dom (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)) )
assume A8: y in { (g * s) where s is FinSequence of NAT : s in S1 } ; :: thesis: y in dom (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1))
consider s being FinSequence of NAT such that
A9: ( y = g * s & s in S1 ) by A8;
S1 c= dom (App ((SignGenOp (f,A,F1)) * E1)) by FINSUB_1:def 5;
then A10: s in dom (App ((SignGenOp (f,A,F1)) * E1)) by A9;
rng s c= dom g

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng s or y in dom g )
assume A11: y in rng s ; :: thesis: y in dom g
consider x being object such that
A12: ( x in dom s & s . x = y ) by A11, FUNCT_1:def 3;
reconsider x = x as Nat by A12;
A13: s . x in dom (((SignGenOp (f,A,F1)) * E1) . x) by A12, A10, Th47;
((SignGenOp (f,A,F1)) * E1) . x <> {} by A12, A10, Th47;
then x in dom ((SignGenOp (f,A,F1)) * E1) by FUNCT_1:def 2;
then ((SignGenOp (f,A,F1)) * E1) . x = SignGen (f,A,(E1 . x)) by Th80;
then dom (((SignGenOp (f,A,F1)) * E1) . x) = dom f by Def11;
hence y in dom g by FUNCT_2:52, A13, A12; :: thesis: verum

end;

then g * s in doms ((SignGenOp (fg,A,((.: g) .: F1))) * gE1) by Th98, A2, A4, A7, A5, A10;
hence y in dom (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1)) by A9, Def9; :: thesis: verum

end;

hence { (g * s) where s is FinSequence of NAT : s in S1 } is Element of Fin (dom (App ((SignGenOp (fg,A,((.: g) .: F1))) * gE1))) by FINSUB_1:def 5; :: thesis: verum