theorem :: EUCLID:74

for n being Nat holds |.(1.REAL n).| = sqrt n by Th45;