thus ( f is natural-valued implies for x being object st x in dom f holds
f . x is natural ) :: thesis: ( ( for x being object st x in dom f holds
f . x is natural ) implies f is natural-valued )
proof
assume A10: f is natural-valued ; :: thesis: for x being object st x in dom f holds
f . x is natural
let x be object ; :: thesis: ( x in dom f implies f . x is natural )
assume A11: x in dom f ; :: thesis: f . x is natural
reconsider f = f as natural-valued Function by A10;
f . x in rng f by A11, FUNCT_1:3;
hence f . x is natural ; :: thesis: verum
end;
assume A12: for x being object st x in dom f holds
f . x is natural ; :: thesis: f is natural-valued
let y be object ; :: according to TARSKI:def 3,VALUED_0:def 6 :: thesis: ( not y in rng f or y in NAT )
assume y in rng f ; :: thesis: y in NAT
then ex x being object st
( x in dom f & y = f . x ) by FUNCT_1:def 3;
then y is natural by A12;
hence y in NAT by ORDINAL1:def 12; :: thesis: verum