let n be Nat; :: thesis: for u, v being Element of (TOP-REAL n) holds u + (0 * v) = u
let u, v be Element of (TOP-REAL n); :: thesis: u + (0 * v) = u
0. (TOP-REAL n) = 0 * v by RLVECT_1:10;
hence u + (0 * v) = u ; :: thesis: verum