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
(Mx2Tran (Rotation (i,j,n,r))) . p = ((((p | (i -' 1)) ^ <*(((p . i) * (cos r)) + ((p . j) * (- (sin r))))*>) ^ ((p /^ i) | ((j -' i) -' 1))) ^ <*(((p . i) * (sin r)) + ((p . j) * (cos r)))*>) ^ (p /^ j)
let i, j, n be Nat; :: thesis: for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n holds
(Mx2Tran (Rotation (i,j,n,r))) . p = ((((p | (i -' 1)) ^ <*(((p . i) * (cos r)) + ((p . j) * (- (sin r))))*>) ^ ((p /^ i) | ((j -' i) -' 1))) ^ <*(((p . i) * (sin r)) + ((p . j) * (cos r)))*>) ^ (p /^ j)
let p be Point of (TOP-REAL n); :: thesis: ( 1 <= i & i < j & j <= n implies (Mx2Tran (Rotation (i,j,n,r))) . p = ((((p | (i -' 1)) ^ <*(((p . i) * (cos r)) + ((p . j) * (- (sin r))))*>) ^ ((p /^ i) | ((j -' i) -' 1))) ^ <*(((p . i) * (sin r)) + ((p . j) * (cos r)))*>) ^ (p /^ j) )
assume that
A1: 1 <= i and
A2: i < j and
A3: j <= n ; :: thesis: (Mx2Tran (Rotation (i,j,n,r))) . p = ((((p | (i -' 1)) ^ <*(((p . i) * (cos r)) + ((p . j) * (- (sin r))))*>) ^ ((p /^ i) | ((j -' i) -' 1))) ^ <*(((p . i) * (sin r)) + ((p . j) * (cos r)))*>) ^ (p /^ j)
set M = Mx2Tran (Rotation (i,j,n,r));
set Mp = (Mx2Tran (Rotation (i,j,n,r))) . p;
set i1 = i -' 1;
set ji = j -' i;
A4: i < n by A2, A3, XXREAL_0:2;
A5: ( i -' 1 < (i -' 1) + 1 & i -' 1 = i - 1 ) by A1, NAT_1:13, XREAL_1:233;
A9: len ((Mx2Tran (Rotation (i,j,n,r))) . p) = n by CARD_1:def 7;
then A10: len (((Mx2Tran (Rotation (i,j,n,r))) . p) | (i -' 1)) = i -' 1 by A5, A4, FINSEQ_1:59, XXREAL_0:2;
A11: len p = n by CARD_1:def 7;
then A12: len (p /^ i) = n - i by A4, RFINSEQ:def 1;
A13: j -' i = j - i by A2, XREAL_1:233;
then A14: ( (j -' i) -' 1 < ((j -' i) -' 1) + 1 & j -' i <= n - i ) by A3, NAT_1:13, XREAL_1:6;
j - i > i - i by A2, XREAL_1:8;
then A15: (j -' i) -' 1 = (j -' i) - 1 by A13, NAT_1:14, XREAL_1:233;
A16: len (p /^ j) = n - j by A3, A11, RFINSEQ:def 1;
A17: len (((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i) = n - i by A9, A4, RFINSEQ:def 1;
then A18: len ((((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i) | ((j -' i) -' 1)) = (j -' i) -' 1 by A14, A15, FINSEQ_1:59, XXREAL_0:2;
A19: (j -' i) -' 1 < n - i by A14, A15, XXREAL_0:2;
len ((p /^ i) | ((j -' i) -' 1)) = (j -' i) -' 1 by A14, A15, A12, FINSEQ_1:59, XXREAL_0:2;
then A28: (((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i) | ((j -' i) -' 1) = (p /^ i) | ((j -' i) -' 1) by A20, A18;
A29: len (((Mx2Tran (Rotation (i,j,n,r))) . p) /^ j) = n - j by A3, A9, RFINSEQ:def 1;
then A34: ((Mx2Tran (Rotation (i,j,n,r))) . p) /^ j = p /^ j by A16, A29;
len (p | (i -' 1)) = i -' 1 by A5, A11, A4, FINSEQ_1:59, XXREAL_0:2;
then A35: ((Mx2Tran (Rotation (i,j,n,r))) . p) | (i -' 1) = p | (i -' 1) by A6, A10;
A36: ((Mx2Tran (Rotation (i,j,n,r))) . p) . i = ((p . i) * (cos r)) + ((p . j) * (- (sin r))) by A1, A2, A3, Th21;
(Mx2Tran (Rotation (i,j,n,r))) . p = @ (@ ((Mx2Tran (Rotation (i,j,n,r))) . p)) ;
then (Mx2Tran (Rotation (i,j,n,r))) . p = ((((((Mx2Tran (Rotation (i,j,n,r))) . p) | (i -' 1)) ^ <*(((Mx2Tran (Rotation (i,j,n,r))) . p) . i)*>) ^ ((((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i) | ((j -' i) -' 1))) ^ <*(((Mx2Tran (Rotation (i,j,n,r))) . p) . j)*>) ^ (((Mx2Tran (Rotation (i,j,n,r))) . p) /^ j) by A1, A2, A3, A9, FINSEQ_7:1;
hence (Mx2Tran (Rotation (i,j,n,r))) . p = ((((p | (i -' 1)) ^ <*(((p . i) * (cos r)) + ((p . j) * (- (sin r))))*>) ^ ((p /^ i) | ((j -' i) -' 1))) ^ <*(((p . i) * (sin r)) + ((p . j) * (cos r)))*>) ^ (p /^ j) by A1, A2, A3, A34, A28, A35, A36, Th22; :: thesis: verum