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