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

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

A2: rng fs is finite ;

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

deffunc H

A2: rng fs is finite ;

A1: { H

{ t where t is transition of PTN : S

hence { t where t is transition of PTN : t in rng fs } is finite Subset of the carrier' of PTN by A1; :: thesis: verum