let n be Nat; :: 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 (doms (n,(card F))) holds { (s * p) where s is FinSequence of NAT : s in S } is Element of Fin (doms (n,(card F)))
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 (doms (n,(card F))) holds { (s * p) where s is FinSequence of NAT : s in S } is Element of Fin (doms (n,(card F)))
let E be Enumeration of F; :: thesis: for p being Permutation of (dom E)
for S being Element of Fin (doms (n,(card F))) holds { (s * p) where s is FinSequence of NAT : s in S } is Element of Fin (doms (n,(card F)))
let p be Permutation of (dom E); :: thesis: for S being Element of Fin (doms (n,(card F))) holds { (s * p) where s is FinSequence of NAT : s in S } is Element of Fin (doms (n,(card F)))
reconsider Ep = E * p as Enumeration of F by Th109;
set D = the non empty set ;
set f = the n -element FinSequence of the non empty set ;
set A = the BinOp of the non empty set ;
A1: len the n -element FinSequence of the non empty set = n by CARD_1:def 7;
let S be Element of Fin (doms (n,(card F))); :: thesis: { (s * p) where s is FinSequence of NAT : s in S } is Element of Fin (doms (n,(card F)))
{ (s * p) where s is FinSequence of NAT : s in S } c= doms (n,(card F))

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 doms (n,(card F)) )
assume y in { (s * p) where s is FinSequence of NAT : s in S } ; :: thesis: y in doms (n,(card F))
then consider s being FinSequence of NAT such that
A2: ( y = s * p & s in S ) ;
S c= doms (n,(card F)) by FINSUB_1:def 5;
then S c= dom (App ((SignGenOp ( the n -element FinSequence of the non empty set , the BinOp of the non empty set ,F)) * E)) by A1, Lm3;
then s in dom (App ((SignGenOp ( the n -element FinSequence of the non empty set , the BinOp of the non empty set ,F)) * E)) by A2;
then s * p in doms ((SignGenOp ( the n -element FinSequence of the non empty set , the BinOp of the non empty set ,F)) * Ep) by Th110;
hence y in doms (n,(card F)) by A2, A1, Th106; :: thesis: verum

end;

hence { (s * p) where s is FinSequence of NAT : s in S } is Element of Fin (doms (n,(card F))) by FINSUB_1:def 5; :: thesis: verum