let i, n be Nat; :: thesis: for p being Point of (TOP-REAL n) st i in Seg n holds
((Mx2Tran (AxialSymmetry (i,n))) . p) . i = - (p . i)
let p be Point of (TOP-REAL n); :: thesis: ( i in Seg n implies ((Mx2Tran (AxialSymmetry (i,n))) . p) . i = - (p . i) )
set A = AxialSymmetry (i,n);
set M = Mx2Tran (AxialSymmetry (i,n));
set Mp = (Mx2Tran (AxialSymmetry (i,n))) . p;
set S = Seg n;
assume A1: i in Seg n ; :: thesis: ((Mx2Tran (AxialSymmetry (i,n))) . p) . i = - (p . i)
then ( 1 <= i & i <= n ) by FINSEQ_1:1;
hence ((Mx2Tran (AxialSymmetry (i,n))) . p) . i = (@ p) "*" (Col ((AxialSymmetry (i,n)),i)) by MATRTOP1:18
.= - (p . i) by A1, Th6 ;
:: thesis: verum