let r be Real; :: thesis: for i, j, n being Nat
for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n holds
(@ p) "*" (Col ((Rotation (i,j,n,r)),j)) = ((p . i) * (sin r)) + ((p . j) * (cos r))
let i, j, n be Nat; :: thesis: for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n holds
(@ p) "*" (Col ((Rotation (i,j,n,r)),j)) = ((p . i) * (sin r)) + ((p . j) * (cos r))
let p be Point of (TOP-REAL n); :: thesis: ( 1 <= i & i < j & j <= n implies (@ p) "*" (Col ((Rotation (i,j,n,r)),j)) = ((p . i) * (sin r)) + ((p . j) * (cos r)) )
assume that
A1: 1 <= i and
A2: i < j and
A3: j <= n ; :: thesis: (@ p) "*" (Col ((Rotation (i,j,n,r)),j)) = ((p . i) * (sin r)) + ((p . j) * (cos r))
set O = Rotation (i,j,n,r);
set C = Col ((Rotation (i,j,n,r)),j);
set S = Seg n;
1 <= j by A1, A2, XXREAL_0:2;
then A4: j in Seg n by A3;
A5: len (Rotation (i,j,n,r)) = n by MATRIX_0:25;
then A6: dom (Rotation (i,j,n,r)) = Seg n by FINSEQ_1:def 3;
then A7: (Col ((Rotation (i,j,n,r)),j)) . j = (Rotation (i,j,n,r)) * (j,j) by A4, MATRIX_0:def 8;
A8: i <= n by A2, A3, XXREAL_0:2;
then A9: i in Seg n by A1;
then A10: (Col ((Rotation (i,j,n,r)),j)) . i = (Rotation (i,j,n,r)) * (i,j) by A6, MATRIX_0:def 8;
( len p = n & len (Col ((Rotation (i,j,n,r)),j)) = n ) by A5, CARD_1:def 7;
then len (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) = n by MATRIX_3:6;
then A11: dom (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) = Seg n by FINSEQ_1:def 3;
then A12: i in dom (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) by A1, A8;
A13: Indices (Rotation (i,j,n,r)) = [:(Seg n),(Seg n):] by MATRIX_0:24;
for k being Nat st k in dom (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) & k <> i & k <> j holds
(mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) . k = 0. F_Real

proof

let k be Nat; :: thesis: ( k in dom (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) & k <> i & k <> j implies (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) . k = 0. F_Real )
assume that
A14: k in dom (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) and
A15: k <> i and
A16: k <> j ; :: thesis: (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) . k = 0. F_Real
not k in {i,j} by A15, A16, TARSKI:def 2;
then A17: {k,j} <> {i,j} by TARSKI:def 2;
reconsider pk = (@ p) . k as Element of F_Real by XREAL_0:def 1;
A18: [k,j] in Indices (Rotation (i,j,n,r)) by A4, A11, A13, A14, ZFMISC_1:87;
(Col ((Rotation (i,j,n,r)),j)) . k = (Rotation (i,j,n,r)) * (k,j) by A6, A11, A14, MATRIX_0:def 8;
hence (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) . k = pk * ((Rotation (i,j,n,r)) * (k,j)) by A14, FVSUM_1:60
.= pk * (0. F_Real) by A1, A2, A3, A16, A17, A18, Def3
.= 0. F_Real ;
:: thesis: verum

end;

then A19: Sum (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) = ((mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) /. i) + ((mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) /. j) by A2, A4, A9, A11, MATRIX15:7;
reconsider pii = (@ p) . i, pj = (@ p) . j as Element of F_Real by XREAL_0:def 1;
A20: (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) /. i = (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) . i by A9, A11, PARTFUN1:def 6
.= pii * ((Rotation (i,j,n,r)) * (i,j)) by A10, A12, FVSUM_1:60
.= (p . i) * (sin r) by A1, A2, A3, Def3 ;
(mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) /. j = (mlt ((@ p),(Col ((Rotation (i,j,n,r)),j)))) . j by A4, A11, PARTFUN1:def 6
.= pj * ((Rotation (i,j,n,r)) * (j,j)) by A4, A7, A11, FVSUM_1:60
.= (p . j) * (cos r) by A1, A2, A3, Def3 ;
hence (@ p) "*" (Col ((Rotation (i,j,n,r)),j)) = ((p . i) * (sin r)) + ((p . j) * (cos r)) by A19, A20; :: thesis: verum