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

proof

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

end;

assume A6: for x being object st x in dom f holds
f . x is ext-real ; :: thesis: f is ext-real-valued
let y be object ; :: 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 ex x being object st
( x in dom f & y = f . x ) by FUNCT_1:def 3;
then y is ext-real by A6;
hence y in ExtREAL by XXREAL_0:def 1; :: thesis: verum