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

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

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

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

suppose x in dom f ; :: thesis: f . b₁ is rational

then f . x in rng f by FUNCT_1:def 3;
hence f . x is rational by A1; :: thesis: verum

end;

suppose not x in dom f ; :: thesis: f . b₁ is rational

hence f . x is rational by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

assume A2: for x being object holds f . x is rational ; :: thesis: f is RAT -valued
let y be object ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not y in rng f or y in RAT )
assume y in rng f ; :: thesis: y in RAT
then consider x being object such that
x in dom f and
A3: f . x = y by FUNCT_1:def 3;
f . x is rational by A2;
hence y in RAT by A3, RAT_1:def 2; :: thesis: verum