let f be non-zero PartFunc of NAT ,REAL ; :: thesis: rng f c= REAL \ {0 }
not {} in rng f by RELAT_1:def 9;
hence rng f c= REAL \ {0 } by ZFMISC_1:40; :: thesis: verum