let r be Real; :: according to PARTFUN3:def 4 :: thesis: ( not r in rng (f | n) or 0 <= r )
assume r in rng (f | n) ; :: thesis: 0 <= r
then ex i being object st
( i in dom (f | n) & (f | n) . i = r ) by FUNCT_1:def 3;
hence 0 <= r ; :: thesis: verum