let D be non empty set ; :: thesis: for A being BinOp of D
for f being FinSequence of D
for F being finite set
for E being Enumeration of F
for p being Permutation of (dom E)
for S being Element of Fin (dom (App ((SignGenOp (f,A,F)) * E))) holds { (s * p) where s is FinSequence of NAT : s in S } is Element of Fin (dom (App ((SignGenOp (f,A,F)) * (E * p))))
let A be BinOp of D; :: thesis: for f being FinSequence of D
for F being finite set
for E being Enumeration of F
for p being Permutation of (dom E)
for S being Element of Fin (dom (App ((SignGenOp (f,A,F)) * E))) holds { (s * p) where s is FinSequence of NAT : s in S } is Element of Fin (dom (App ((SignGenOp (f,A,F)) * (E * p))))
let f be FinSequence of D; :: thesis: for F being finite set
for E being Enumeration of F
for p being Permutation of (dom E)
for S being Element of Fin (dom (App ((SignGenOp (f,A,F)) * E))) holds { (s * p) where s is FinSequence of NAT : s in S } is Element of Fin (dom (App ((SignGenOp (f,A,F)) * (E * p))))
let F be finite set ; :: thesis: for E being Enumeration of F
for p being Permutation of (dom E)
for S being Element of Fin (dom (App ((SignGenOp (f,A,F)) * E))) holds { (s * p) where s is FinSequence of NAT : s in S } is Element of Fin (dom (App ((SignGenOp (f,A,F)) * (E * p))))
let E be Enumeration of F; :: thesis: for p being Permutation of (dom E)
for S being Element of Fin (dom (App ((SignGenOp (f,A,F)) * E))) holds { (s * p) where s is FinSequence of NAT : s in S } is Element of Fin (dom (App ((SignGenOp (f,A,F)) * (E * p))))
let p be Permutation of (dom E); :: thesis: for S being Element of Fin (dom (App ((SignGenOp (f,A,F)) * E))) holds { (s * p) where s is FinSequence of NAT : s in S } is Element of Fin (dom (App ((SignGenOp (f,A,F)) * (E * p))))
let S be Element of Fin (dom (App ((SignGenOp (f,A,F)) * E))); :: thesis: { (s * p) where s is FinSequence of NAT : s in S } is Element of Fin (dom (App ((SignGenOp (f,A,F)) * (E * p))))
{ (s * p) where s is FinSequence of NAT : s in S } c= dom (App ((SignGenOp (f,A,F)) * (E * p)))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { (s * p) where s is FinSequence of NAT : s in S } or y in dom (App ((SignGenOp (f,A,F)) * (E * p))) )
assume y in { (s * p) where s is FinSequence of NAT : s in S } ; :: thesis: y in dom (App ((SignGenOp (f,A,F)) * (E * p)))
then consider s being FinSequence of NAT such that
A1: ( y = s * p & s in S ) ;
S c= dom (App ((SignGenOp (f,A,F)) * E)) by FINSUB_1:def 5;
then s in dom (App ((SignGenOp (f,A,F)) * E)) by A1;
then s * p in doms ((SignGenOp (f,A,F)) * (E * p)) by Th110;
hence y in dom (App ((SignGenOp (f,A,F)) * (E * p))) by A1, Def9; :: thesis: verum

end;

hence { (s * p) where s is FinSequence of NAT : s in S } is Element of Fin (dom (App ((SignGenOp (f,A,F)) * (E * p)))) by FINSUB_1:def 5; :: thesis: verum