let u be object ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not u in rng ||.f.|| or u in REAL )
assume u in rng ||.f.|| ; :: thesis: u in REAL
then consider e being object such that
A1: e in dom ||.f.|| and
A2: u = ||.f.|| . e by FUNCT_1:def 3;
||.f.|| . e = ||.(f /. e).|| by A1, Def2;
hence u in REAL by A2; :: thesis: verum