theorem Th45: :: EUCLID:73

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