theorem Th8: :: MATRTOP3:8

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