thus
( f is ext-real-functions-valued implies for x being object st x in dom f holds

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

f . x is ext-real-valued Function ) implies f is ext-real-functions-valued )

f . x is ext-real-valued Function ; :: thesis: f is ext-real-functions-valued

let y be object ; :: according to VALUED_2:def 3,VALUED_2:def 21 :: thesis: ( y in rng f implies y is ext-real-valued Function )

assume y in rng f ; :: thesis: y is ext-real-valued Function

then ex x being object st

( x in dom f & f . x = y ) by FUNCT_1:def 3;

hence y is ext-real-valued Function by A4; :: thesis: verum

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

f . x is ext-real-valued Function ) implies f is ext-real-functions-valued )

proof

assume A4:
for x being object st x in dom f holds
assume A3:
rng f is ext-real-functions-membered
; :: according to VALUED_2:def 21 :: thesis: for x being object st x in dom f holds

f . x is ext-real-valued Function

let x be object ; :: thesis: ( x in dom f implies f . x is ext-real-valued Function )

assume x in dom f ; :: thesis: f . x is ext-real-valued Function

then f . x in rng f by FUNCT_1:def 3;

hence f . x is ext-real-valued Function by A3; :: thesis: verum

end;f . x is ext-real-valued Function

let x be object ; :: thesis: ( x in dom f implies f . x is ext-real-valued Function )

assume x in dom f ; :: thesis: f . x is ext-real-valued Function

then f . x in rng f by FUNCT_1:def 3;

hence f . x is ext-real-valued Function by A3; :: thesis: verum

f . x is ext-real-valued Function ; :: thesis: f is ext-real-functions-valued

let y be object ; :: according to VALUED_2:def 3,VALUED_2:def 21 :: thesis: ( y in rng f implies y is ext-real-valued Function )

assume y in rng f ; :: thesis: y is ext-real-valued Function

then ex x being object st

( x in dom f & f . x = y ) by FUNCT_1:def 3;

hence y is ext-real-valued Function by A4; :: thesis: verum