theorem :: MATRTOP3:41

for n being Nat
for p, q being Point of (TOP-REAL n) st n <> 1 & |.p.| = |.q.| holds
ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is base_rotation & f . p = q )