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