theorem :: MATRTOP3:40

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 rotation & f . p = q & ( AutMt f = AxialSymmetry (n,n) or AutMt f = 1. (F_Real,n) ) )