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