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