A1: dom (fire C) = Funcs (P,NAT) by Th26;
A2: rng (fire C) c= Funcs (P,NAT) by Th26;
m in dom (fire C) by A1, FUNCT_2:8;
then [m,((fire C) . m)] in fire C by FUNCT_1:def 2;
then (fire C) . m in rng (fire C) by XTUPLE_0:def 13;
hence (fire C) . m is marking of P by A2, FUNCT_2:66; :: thesis: verum