theorem Th38: :: EUCLID:66

for n being Nat holds 0.REAL n = 0. (TOP-REAL n)