let i, j, n be Nat; :: thesis: for p being Point of () 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 (); :: 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 ;
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 ;
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 ;
thus (Col ((AxialSymmetry (i,n)),j)) . m = (AxialSymmetry (i,n)) * (m,j) by
.= 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
.= 1. F_Real by A1, A3, A5, Def2 ;
hence p . j = Sum (mlt ((Col ((AxialSymmetry (i,n)),j)),(@ p))) by
.= (@ p) "*" (Col ((AxialSymmetry (i,n)),j)) by FVSUM_1:64 ;
:: thesis: verum