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, Def11;
hence y in RAT by A2, RAT_1:def 2; :: thesis: verum