thus ( f is ext-real-valued implies for x being set st x in dom f holds
f . x is ext-real ) :: thesis: ( ( for x being set st x in dom f holds
f . x is ext-real ) implies f is ext-real-valued )

proof

assume A6: f is ext-real-valued ; :: thesis: for x being set st x in dom f holds
f . x is ext-real
let x be set ; :: thesis: ( x in dom f implies f . x is ext-real )
assume A7: x in dom f ; :: thesis: f . x is ext-real
reconsider f = f as ext-real-valued Function by A6;
f . x in rng f by A7, FUNCT_1:12;
hence f . x is ext-real ; :: thesis: verum

end;

assume A8: for x being set st x in dom f holds
f . x is ext-real ; :: thesis: f is ext-real-valued
let y be set ; :: according to TARSKI:def 3,VALUED_0:def 2 :: thesis: ( not y in rng f or y in ExtREAL )
assume y in rng f ; :: thesis: y in ExtREAL
then consider x being set such that
A9: x in dom f and
A10: y = f . x by FUNCT_1:def 5;
y is ext-real by A8, A9, A10;
hence y in ExtREAL by XXREAL_0:def 1; :: thesis: verum