let i be Nat; :: thesis: ( i in (Seg n) /\ (dom R) implies R . i >= 0 )
assume i in (Seg n) /\ (dom R) ; :: thesis: R . i >= 0
then i in dom R by XBOOLE_0:def 4;
then R . i in rng R by FUNCT_1:def 3;
hence R . i >= 0 by PARTFUN3:def 4; :: thesis: verum