:: deftheorem Def4 defines rotation MATRTOP3:def 4 :
for n being Nat
for f being Function of (TOP-REAL n),(TOP-REAL n) holds
( f is rotation iff for p being Point of (TOP-REAL n) holds |.p.| = |.(f . p).| );