hereby :: thesis: ( ( for x being object st x in dom f holds
f . x is ext-natural ) implies f is ext-natural-valued )

assume A1: f is ext-natural-valued ; :: thesis: for x being object st x in dom f holds
f . x is ext-natural
let x be object ; :: thesis: ( x in dom f implies f . x is ext-natural )
assume x in dom f ; :: thesis: f . x is ext-natural
then f . x in rng f by FUNCT_1:3;
hence f . x is ext-natural by A1; :: thesis: verum

end;

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

now :: thesis: for y being object st y in rng f holds
y in ExtNAT

let y be object ; :: thesis: ( y in rng f implies y in ExtNAT )
assume y in rng f ; :: thesis: y in ExtNAT
then consider x being object such that
A3: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
y is ext-natural by A2, A3;
hence y in ExtNAT ; :: thesis: verum

end;

hence f is ext-natural-valued by TARSKI:def 3; :: thesis: verum