let P be set ; :: thesis: for t being transition of P holds rng (fire t) c= Funcs (P,NAT)

let t be transition of P; :: thesis: rng (fire t) c= Funcs (P,NAT)

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (fire t) or y in Funcs (P,NAT) )

assume y in rng (fire t) ; :: thesis: y in Funcs (P,NAT)

then consider x being object such that

A1: x in dom (fire t) and

A2: y = (fire t) . x by FUNCT_1:def 3;

dom (fire t) = Funcs (P,NAT) by Def8;

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

y = fire (t,m) by A2, Def8;

hence y in Funcs (P,NAT) by FUNCT_2:8; :: thesis: verum

let t be transition of P; :: thesis: rng (fire t) c= Funcs (P,NAT)

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (fire t) or y in Funcs (P,NAT) )

assume y in rng (fire t) ; :: thesis: y in Funcs (P,NAT)

then consider x being object such that

A1: x in dom (fire t) and

A2: y = (fire t) . x by FUNCT_1:def 3;

dom (fire t) = Funcs (P,NAT) by Def8;

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

y = fire (t,m) by A2, Def8;

hence y in Funcs (P,NAT) by FUNCT_2:8; :: thesis: verum