( dom (m1 + m2) = P & rng (m1 + m2) c= NAT ) by FUNCT_2:def 1, RELSET_1:12;
hence m1 + m2 is marking of P by Def1; :: thesis: verum