theorem :: EUCLID:70

for n being Nat holds 0. (TOP-REAL n) = 0* n by Th38;