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
A1: x in dom (f ") and
A2: (f ") . x = y by FUNCT_1:def 3;
(f ") . x = (f . x) " by A1, Def7;
hence y in RAT by A2, RAT_1:def 2; :: thesis: verum