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