for i, n being Nat
for p being Point of (TOP-REAL n) st i in Seg n & n >= 2 holds
ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st
( f is base_rotation & f . p = p +* (i,(- (p . i))) )