let f be Function; :: thesis:

hereby :: thesis:

assume A1: f is natural-valued ; :: thesis:
let x be object ; :: thesis:

suppose x in dom f ; :: thesis:

hence f . x is natural by A1; :: thesis:

end;

suppose not x in dom f ; :: thesis:

hence f . x is natural by FUNCT_1:def 2; :: thesis:

end;

end;

end;

assume for x being object holds f . x is natural ; :: thesis:
then for x being object st x in dom f holds
f . x is natural ;
hence f is natural-valued ; :: thesis: