let x, P be set ; :: thesis: ( x in Funcs P,NAT implies x is marking of P )
assume x in Funcs P,NAT ; :: thesis: x is marking of P
then ex f being Function st
( x = f & dom f = P & rng f c= NAT ) by FUNCT_2:def 2;
hence x is marking of P by Def1; :: thesis: verum