theorem THJC: :: GTARSKI2:3

for n being Nat
for r, s being Real
for u, v, w being Element of (TOP-REAL n) st (r * u) - (r * v) = (s * w) - (s * u) holds
(r + s) * u = (r * v) + (s * w)