let D be Pos_Denum_Set_of_R_EAL; :: thesis: for N being Num of D
for n being Element of NAT holds 0. <= N . n
let N be Num of D; :: thesis: for n being Element of NAT holds 0. <= N . n
let n be Element of NAT ; :: thesis: 0. <= N . n
D = rng N by Def16;
then N . n in D by FUNCT_2:6;
hence 0. <= N . n by Def15; :: thesis: verum