defpred S₁[ set , set ] means ex m being marking of P st
( m = $1 & $2 = fire t,m );
A2: for x being set st x in Funcs P,NAT holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in Funcs P,NAT implies ex y being set st S₁[x,y] )
assume x in Funcs P,NAT ; :: thesis: ex y being set st S₁[x,y]
then reconsider m = x as marking of P by FUNCT_2:121;
take fire t,m ; :: thesis: S₁[x, fire t,m]
thus S₁[x, fire t,m] ; :: thesis: verum

end;

consider f being Function such that
A3: dom f = Funcs P,NAT and
A4: for x being set st x in Funcs P,NAT holds
S₁[x,f . x] from CLASSES1:sch 1(A2);
take f ; :: thesis: ( dom f = Funcs P,NAT & ( for m being marking of P holds f . m = fire t,m ) )
thus dom f = Funcs P,NAT by A3; :: thesis: for m being marking of P holds f . m = fire t,m
let m be marking of P; :: thesis: f . m = fire t,m
m in Funcs P,NAT by FUNCT_2:11;
then S₁[m,f . m] by A4;
hence f . m = fire t,m ; :: thesis: verum