defpred S_{1}[ set ] means $1 in rng fs;

deffunc H_{1}( set ) -> set = $1;

A2: rng fs is finite ;

A1: { H_{1}(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_{1}[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

deffunc H

A2: rng fs is finite ;

A1: { H

{ p where p is place of PTN : S

hence { p where p is place of PTN : p in rng fs } is finite Subset of PTN by A1; :: thesis: verum