let r be Real; :: according to PARTFUN3:def 4 :: thesis: ( not r in rng invNAT or 0 <= r )
assume r in rng invNAT ; :: thesis: 0 <= r
then consider p being object such that
A1: ( p in dom invNAT & r = invNAT . p ) by FUNCT_1:def 3;
reconsider p = p as Nat by A1;
r = 1 / p by DefRec, A1;
hence 0 <= r ; :: thesis: verum