reconsider p = NAT --> 1 as PartFunc of NAT,REAL by FUNCOP_1:46;
take p ; :: thesis: p is non-zero
rng p = {1} by FUNCOP_1:8;
hence not 0 in rng p by TARSKI:def 1; :: according to RELAT_1:def 9 :: thesis: verum