let r be Real; :: thesis: for i, j, k, n being Nat
for p being Point of () 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 () 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 (); :: 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 ;
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 ;
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 ;
not k in {i,j} by ;
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
.= 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
.= 1. F_Real by A1, A3, A5, Def3 ;
hence p . k = Sum (mlt ((Col ((Rotation (i,j,n,r)),k)),(@ p))) by
.= (@ p) "*" (Col ((Rotation (i,j,n,r)),k)) by FVSUM_1:64 ;
:: thesis: verum