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

proof

let x be object ; :: thesis: ( x in Funcs (P,NAT) implies ex y being object st S₁[x,y] )
assume x in Funcs (P,NAT) ; :: thesis: ex y being object st S₁[x,y]
then reconsider m = x as marking of P by FUNCT_2:66;
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
A2: dom f = Funcs (P,NAT) and
A3: for x being object st x in Funcs (P,NAT) holds
S₁[x,f . x] from CLASSES1:sch 1(A1);
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 A2; :: 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:8;
then S₁[m,f . m] by A3;
hence f . m = fire (t,m) ; :: thesis: verum