for X being set
for n being Nat
for p being Point of (TOP-REAL n)
for f being rotation Function of (TOP-REAL n),(TOP-REAL n) st f is X -support-yielding & ( for i being Nat st i in X /\ (Seg n) holds
p . i = 0 ) holds
f . p = p