theorem Th9: :: MATRTOP3:9

for i, n being Nat
for p being Point of (TOP-REAL n) st i in Seg n holds
((Mx2Tran (AxialSymmetry (i,n))) . p) . i = - (p . i)