theorem THJE: :: GTARSKI2:2

for n being Nat
for u, v being Element of (TOP-REAL n) holds u + (0 * v) = u