let r be Real; :: thesis: for i, j, k, n being Nat
for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n & k in Seg n & k <> i & k <> j holds
(@ p) "*" (Col ((Rotation (i,j,n,r)),k)) = p . k
let i, j, k, n be Nat; :: thesis: for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n & k in Seg n & k <> i & k <> j holds
(@ p) "*" (Col ((Rotation (i,j,n,r)),k)) = p . k
let p be Point of (TOP-REAL n); :: thesis: ( 1 <= i & i < j & j <= n & k in Seg n & k <> i & k <> j implies (@ p) "*" (Col ((Rotation (i,j,n,r)),k)) = p . k )
set S = Seg n;
assume that
A1: ( 1 <= i & i < j & j <= n ) and
A2: k in Seg n and
A3: ( k <> i & k <> j ) ; :: thesis: (@ p) "*" (Col ((Rotation (i,j,n,r)),k)) = p . k
set O = Rotation (i,j,n,r);
set C = Col ((Rotation (i,j,n,r)),k);
A4: Indices (Rotation (i,j,n,r)) = [:(Seg n),(Seg n):] by MATRIX_0:24;
then A5: [k,k] in Indices (Rotation (i,j,n,r)) by A2, ZFMISC_1:87;
A6: len (Rotation (i,j,n,r)) = n by MATRIX_0:25;
then A7: dom (Rotation (i,j,n,r)) = Seg n by FINSEQ_1:def 3;
len (Col ((Rotation (i,j,n,r)),k)) = n by A6, MATRIX_0:def 8;
then A8: dom (Col ((Rotation (i,j,n,r)),k)) = Seg n by FINSEQ_1:def 3;

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

let m be Nat; :: thesis: ( m in dom (Col ((Rotation (i,j,n,r)),k)) & m <> k implies (Col ((Rotation (i,j,n,r)),k)) . m = 0. F_Real )
assume that
A10: m in dom (Col ((Rotation (i,j,n,r)),k)) and
A11: m <> k ; :: thesis: (Col ((Rotation (i,j,n,r)),k)) . m = 0. F_Real
A12: [m,k] in Indices (Rotation (i,j,n,r)) by A2, A4, A8, A10, ZFMISC_1:87;
not k in {i,j} by A3, TARSKI:def 2;
then A13: {m,k} <> {i,j} by TARSKI:def 2;
thus (Col ((Rotation (i,j,n,r)),k)) . m = (Rotation (i,j,n,r)) * (m,k) by A7, A8, A10, MATRIX_0:def 8
.= 0. F_Real by A1, A11, A12, A13, Def3 ; :: thesis: verum

end;

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