theorem MLT2: :: ZMODLAT1:95

for n being Nat holds 1. (INT.Ring,n) = 1. (F_Real,n)