let u be set ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not u in proj2 ||.f.|| or u in REAL )
assume u in rng ||.f.|| ; :: thesis: u in REAL
then consider e being set such that
W1: e in dom ||.f.|| and
W2: u = ||.f.|| . e by FUNCT_1:def 5;
||.f.|| . e = ||.(f /. e).|| by W1, Def1;
hence u in REAL by W2; :: thesis: verum