defpred S₁[ set ] means $1 in rng fs;
deffunc H₁( set ) -> set = $1;
A2: rng fs is finite ;
A1: { H₁(p) where p is place of PTN : p in rng fs } is finite from FRAENKEL:sch 21(A2);
{ p where p is place of PTN : S₁[p] } is Subset of the carrier of PTN from DOMAIN_1:sch 7();
hence { p where p is place of PTN : p in rng fs } is finite Subset of PTN by A1; :: thesis: verum