for n being Nat holds |.(1* n).| = sqrt n