A1: ( dom (fire C) = Funcs P,NAT & rng (fire C) c= Funcs P,NAT ) by Th40;
then m in dom (fire C) by 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 A1, FUNCT_2:121; :: thesis: verum