let i, j, n be Nat; :: thesis: 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
let p be Point of (TOP-REAL n); :: thesis: ( i in Seg n & j in Seg n & i <> j implies (@ p) "*" (Col ((AxialSymmetry (i,n)),j)) = p . j )
set S = Seg n;
assume that
A1: i in Seg n and
A2: j in Seg n and
A3: i <> j ; :: thesis: (@ p) "*" (Col ((AxialSymmetry (i,n)),j)) = p . j
set A = AxialSymmetry (i,n);
set C = Col ((AxialSymmetry (i,n)),j);
A4: Indices (AxialSymmetry (i,n)) = [:(Seg n),(Seg n):] by MATRIX_0:24;
then A5: [j,j] in Indices (AxialSymmetry (i,n)) by A2, ZFMISC_1:87;
A6: len (AxialSymmetry (i,n)) = n by MATRIX_0:25;
then A7: dom (AxialSymmetry (i,n)) = Seg n by FINSEQ_1:def 3;
len (Col ((AxialSymmetry (i,n)),j)) = n by A6, MATRIX_0:def 8;
then A8: dom (Col ((AxialSymmetry (i,n)),j)) = Seg n by FINSEQ_1:def 3;

A9: now :: thesis: for m being Nat st m in dom (Col ((AxialSymmetry (i,n)),j)) & m <> j holds
(Col ((AxialSymmetry (i,n)),j)) . m = 0. F_Real

let m be Nat; :: thesis: ( m in dom (Col ((AxialSymmetry (i,n)),j)) & m <> j implies (Col ((AxialSymmetry (i,n)),j)) . m = 0. F_Real )
assume that
A10: m in dom (Col ((AxialSymmetry (i,n)),j)) and
A11: m <> j ; :: thesis: (Col ((AxialSymmetry (i,n)),j)) . m = 0. F_Real
A12: [m,j] in Indices (AxialSymmetry (i,n)) by A2, A4, A8, A10, ZFMISC_1:87;
thus (Col ((AxialSymmetry (i,n)),j)) . m = (AxialSymmetry (i,n)) * (m,j) by A7, A8, A10, MATRIX_0:def 8
.= 0. F_Real by A1, A11, A12, Def2 ; :: thesis: verum

end;

len p = n by CARD_1:def 7;
then A13: dom p = Seg n by FINSEQ_1:def 3;
(Col ((AxialSymmetry (i,n)),j)) . j = (AxialSymmetry (i,n)) * (j,j) by A2, A7, MATRIX_0:def 8
.= 1. F_Real by A1, A3, A5, Def2 ;
hence p . j = Sum (mlt ((Col ((AxialSymmetry (i,n)),j)),(@ p))) by A2, A8, A9, A13, MATRIX_3:17
.= (@ p) "*" (Col ((AxialSymmetry (i,n)),j)) by FVSUM_1:64 ;
:: thesis: verum