let i, n be Nat; :: thesis: for p being Point of () st i in Seg n holds
(@ p) "*" (Col ((AxialSymmetry (i,n)),i)) = - (p . i)

let p be Point of (); :: thesis: ( i in Seg n implies (@ p) "*" (Col ((AxialSymmetry (i,n)),i)) = - (p . i) )
set S = Seg n;
assume A1: i in Seg n ; :: thesis: (@ p) "*" (Col ((AxialSymmetry (i,n)),i)) = - (p . i)
reconsider pI = (@ p) . i as Element of F_Real by XREAL_0:def 1;
set A = AxialSymmetry (i,n);
set C = Col ((AxialSymmetry (i,n)),i);
A2: len (AxialSymmetry (i,n)) = n by MATRIX_0:25;
then A3: dom (AxialSymmetry (i,n)) = Seg n by FINSEQ_1:def 3;
then A4: (Col ((AxialSymmetry (i,n)),i)) . i = (AxialSymmetry (i,n)) * (i,i) by ;
( len p = n & len (Col ((AxialSymmetry (i,n)),i)) = n ) by ;
then len (mlt ((@ p),(Col ((AxialSymmetry (i,n)),i)))) = n by MATRIX_3:6;
then A5: dom (mlt ((@ p),(Col ((AxialSymmetry (i,n)),i)))) = Seg n by FINSEQ_1:def 3;
A6: Indices (AxialSymmetry (i,n)) = [:(Seg n),(Seg n):] by MATRIX_0:24;
A7: for k being Nat st k in dom (mlt ((@ p),(Col ((AxialSymmetry (i,n)),i)))) & k <> i holds
(mlt ((@ p),(Col ((AxialSymmetry (i,n)),i)))) . k = 0. F_Real
proof
let k be Nat; :: thesis: ( k in dom (mlt ((@ p),(Col ((AxialSymmetry (i,n)),i)))) & k <> i implies (mlt ((@ p),(Col ((AxialSymmetry (i,n)),i)))) . k = 0. F_Real )
assume that
A8: k in dom (mlt ((@ p),(Col ((AxialSymmetry (i,n)),i)))) and
A9: k <> i ; :: thesis: (mlt ((@ p),(Col ((AxialSymmetry (i,n)),i)))) . k = 0. F_Real
(@ p) . k in REAL by XREAL_0:def 1;
then reconsider pk = (@ p) . k as Element of F_Real ;
A10: [k,i] in Indices (AxialSymmetry (i,n)) by ;
(Col ((AxialSymmetry (i,n)),i)) . k = (AxialSymmetry (i,n)) * (k,i) by ;
hence (mlt ((@ p),(Col ((AxialSymmetry (i,n)),i)))) . k = pk * ((AxialSymmetry (i,n)) * (k,i)) by
.= pk * () by A1, A9, A10, Def2
.= 0. F_Real ;
:: thesis: verum
end;
thus (@ p) "*" (Col ((AxialSymmetry (i,n)),i)) = (mlt ((@ p),(Col ((AxialSymmetry (i,n)),i)))) . i by
.= pI * ((AxialSymmetry (i,n)) * (i,i)) by
.= pI * (- ()) by
.= pI * (- 1)
.= - (p . i) ; :: thesis: verum