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