let n be Element of NAT ; :: thesis: - (0. (TOP-REAL n)) = 0. (TOP-REAL n)
(0. (TOP-REAL n)) + (0. (TOP-REAL n)) = 0. (TOP-REAL n) by RLVECT_1:4;
hence - (0. (TOP-REAL n)) = 0. (TOP-REAL n) by RLVECT_1:6; :: thesis: verum