theorem Th41: :: BORSUK_7:51
for s being Real
for p being Point of (TOP-REAL 2) holds |.((Rotate s) . p).| = |.p.|