take s = NAT --> 1r ; :: thesis: s is non-zero
rng s = {1} by FUNCOP_1:14;
hence not 0 in rng s by TARSKI:def 1; :: according to RELAT_1:def 9 :: thesis: verum