let n be Nat; :: thesis: for p being Point of (TOP-REAL n)
for r being real number st r >= 0 holds
r * p in halfline ((0. (TOP-REAL n)),p)
let p be Point of (TOP-REAL n); :: thesis: for r being real number st r >= 0 holds
r * p in halfline ((0. (TOP-REAL n)),p)
let r be real number ; :: thesis: ( r >= 0 implies r * p in halfline ((0. (TOP-REAL n)),p) )
A1: n in NAT by ORDINAL1:def 12;
assume A2: r >= 0 ; :: thesis: r * p in halfline ((0. (TOP-REAL n)),p)
( (1 - r) * (0. (TOP-REAL n)) = 0. (TOP-REAL n) & (0. (TOP-REAL n)) + (r * p) = r * p ) by RLVECT_1:4, RLVECT_1:10;
hence r * p in halfline ((0. (TOP-REAL n)),p) by A1, A2, TOPREAL9:26; :: thesis: verum