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 set ; :: 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 set such that
A1: x in dom (fire t) and
A2: y = (fire t) . x by FUNCT_1:def 5;
dom (fire t) = Funcs P,NAT by Def9;
then reconsider m = x as marking of P by A1, FUNCT_2:121;
y = fire t,m by A2, Def9;
hence y in Funcs P,NAT by FUNCT_2:11; :: thesis: verum