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;

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

(@ 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

len p = n
by CARD_1:def 7;(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;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

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