defpred S_{1}[ 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_{1}[x,y]

A2: dom f = Funcs (P,NAT) and

A3: for x being object st x in Funcs (P,NAT) holds

S_{1}[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_{1}[m,f . m]
by A3;

hence f . m = fire (t,m) ; :: thesis: verum

( m = $1 & $2 = fire (t,m) );

A1: for x being object st x in Funcs (P,NAT) holds

ex y being object st S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in Funcs (P,NAT) implies ex y being object st S_{1}[x,y] )

assume x in Funcs (P,NAT) ; :: thesis: ex y being object st S_{1}[x,y]

then reconsider m = x as marking of P by FUNCT_2:66;

take fire (t,m) ; :: thesis: S_{1}[x, fire (t,m)]

thus S_{1}[x, fire (t,m)]
; :: thesis: verum

end;assume x in Funcs (P,NAT) ; :: thesis: ex y being object st S

then reconsider m = x as marking of P by FUNCT_2:66;

take fire (t,m) ; :: thesis: S

thus S

A2: dom f = Funcs (P,NAT) and

A3: for x being object st x in Funcs (P,NAT) holds

S

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

hence f . m = fire (t,m) ; :: thesis: verum