theorem Th59: :: PRE_POLY:61

for X being set
for f being Function of X,NAT holds f in NatMinor f