1 in NAT
;

then 1 in REAL by NUMBERS:19;

then 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 ORDINAL1:def 15 :: thesis: verum

then 1 in REAL by NUMBERS:19;

then 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 ORDINAL1:def 15 :: thesis: verum