let X be set ; :: thesis: for f being Function of X,NAT holds f in NatMinor f
let f be Function of X,NAT ; :: thesis: f in NatMinor f
dom f = X by FUNCT_2:def 1;
then A1: f is ManySortedSet of by PARTFUN1:def 4;
for x being set st x in X holds
f . x <= f . x ;
hence f in NatMinor f by A1, Def17; :: thesis: verum