for i, j, n being Nat
for p being Point of (TOP-REAL n) st i in Seg n & j in Seg n & i <> j holds
(@ p) "*" (Col ((AxialSymmetry (i,n)),j)) = p . j