let P be set ; :: thesis: for m being marking of P holds m in Funcs P,NAT
let m be marking of P; :: thesis: m in Funcs P,NAT
A1: dom m = P by Def1;
rng m c= NAT by Def1;
hence m in Funcs P,NAT by A1, FUNCT_2:def 2; :: thesis: verum