let f be Function; :: thesis: ( f is ext-real-valued iff for x being object holds f . x is ext-real )

hereby :: thesis: ( ( for x being object holds f . x is ext-real ) implies f is ext-real-valued )

assume A1: f is ext-real-valued ; :: thesis: for x being object holds f . b₂ is ext-real
let x be object ; :: thesis: f . b₁ is ext-real

per cases ( x in dom f or not x in dom f ) ;

suppose x in dom f ; :: thesis: f . b₁ is ext-real

hence f . x is ext-real by A1; :: thesis: verum

end;

suppose not x in dom f ; :: thesis: f . b₁ is ext-real

hence f . x is ext-real by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

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