thus ( f is rational-functions-valued implies for x being set st x in dom f holds
f . x is rational-valued Function ) :: thesis: ( ( for x being set st x in dom f holds
f . x is rational-valued Function ) implies f is rational-functions-valued )

proof

assume A7: rng f is rational-functions-membered ; :: according to VALUED_2:def 23 :: thesis: for x being set st x in dom f holds
f . x is rational-valued Function
let x be set ; :: thesis: ( x in dom f implies f . x is rational-valued Function )
assume x in dom f ; :: thesis: f . x is rational-valued Function
then f . x in rng f by FUNCT_1:def 5;
hence f . x is rational-valued Function by A7; :: thesis: verum

end;

assume A8: for x being set st x in dom f holds
f . x is rational-valued Function ; :: thesis: f is rational-functions-valued
let y be set ; :: according to VALUED_2:def 5,VALUED_2:def 23 :: thesis: ( y in rng f implies y is rational-valued Function )
assume y in rng f ; :: thesis: y is rational-valued Function
then ex x being set st
( x in dom f & f . x = y ) by FUNCT_1:def 5;
hence y is rational-valued Function by A8; :: thesis: verum