for x being object
for n being Nat holds (0.REAL n) +* (x,0) = 0.REAL n