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
for x being set st x in X holds
f . x <= f . x ;
hence f in NatMinor f by Def14; :: thesis: verum