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

proof

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

end;

assume A12: for x being set st x in dom f holds
f . x is rational ; :: thesis: f is rational-valued
let y be set ; :: according to TARSKI:def 3,VALUED_0:def 4 :: thesis: ( not y in rng f or y in RAT )
assume y in rng f ; :: thesis: y in RAT
then ex x being set st
( x in dom f & y = f . x ) by FUNCT_1:def 5;
then y is rational by A12;
hence y in RAT by RAT_1:def 2; :: thesis: verum