A1: dom (fire C) = Funcs P,NAT by Th40;
A2: rng (fire C) c= Funcs P,NAT by Th40;
m in dom (fire C) by A1, FUNCT_2:11;
then [m,((fire C) . m)] in fire C by FUNCT_1:def 4;
then (fire C) . m in rng (fire C) by RELAT_1:def 5;
hence (fire C) . m is marking of P by A2, FUNCT_2:121; :: thesis: verum