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;

A6: now :: thesis: for k being Nat st 1 <= k & k <= i -' 1 holds
(((Mx2Tran (Rotation (i,j,n,r))) . p) | (i -' 1)) . k = (p | (i -' 1)) . k

let k be Nat; :: thesis: ( 1 <= k & k <= i -' 1 implies (((Mx2Tran (Rotation (i,j,n,r))) . p) | (i -' 1)) . k = (p | (i -' 1)) . k )
assume that
1 <= k and
A7: k <= i -' 1 ; :: thesis: (((Mx2Tran (Rotation (i,j,n,r))) . p) | (i -' 1)) . k = (p | (i -' 1)) . k
A8: ( (((Mx2Tran (Rotation (i,j,n,r))) . p) | (i -' 1)) . k = ((Mx2Tran (Rotation (i,j,n,r))) . p) . k & (p | (i -' 1)) . k = p . k ) by A7, FINSEQ_3:112;
k < i by A5, A7, XXREAL_0:2;
hence (((Mx2Tran (Rotation (i,j,n,r))) . p) | (i -' 1)) . k = (p | (i -' 1)) . k by A1, A2, A3, A8, Th20; :: thesis: verum

end;

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;

A20: now :: thesis: for k being Nat st 1 <= k & k <= (j -' i) -' 1 holds
((((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i) | ((j -' i) -' 1)) . k = ((p /^ i) | ((j -' i) -' 1)) . k

let k be Nat; :: thesis: ( 1 <= k & k <= (j -' i) -' 1 implies ((((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i) | ((j -' i) -' 1)) . k = ((p /^ i) | ((j -' i) -' 1)) . k )
assume that
A21: 1 <= k and
A22: k <= (j -' i) -' 1 ; :: thesis: ((((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i) | ((j -' i) -' 1)) . k = ((p /^ i) | ((j -' i) -' 1)) . k
A23: ((p /^ i) | ((j -' i) -' 1)) . k = (p /^ i) . k by A22, FINSEQ_3:112;
A24: k <= n - i by A19, A22, XXREAL_0:2;
then k in dom (((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i) by A17, A21, FINSEQ_3:25;
then A25: (((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i) . k = ((Mx2Tran (Rotation (i,j,n,r))) . p) . (i + k) by A9, A4, RFINSEQ:def 1;
k < ((j -' i) -' 1) + 1 by A22, NAT_1:13;
then A26: i + k < i + (j -' i) by A15, XREAL_1:8;
k in dom (p /^ i) by A12, A21, A24, FINSEQ_3:25;
then A27: (p /^ i) . k = p . (i + k) by A11, A4, RFINSEQ:def 1;
( k + i <> i & ((((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i) | ((j -' i) -' 1)) . k = (((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i) . k ) by A21, A22, FINSEQ_3:112, NAT_1:14;
hence ((((Mx2Tran (Rotation (i,j,n,r))) . p) /^ i) | ((j -' i) -' 1)) . k = ((p /^ i) | ((j -' i) -' 1)) . k by A1, A2, A3, A13, A25, A26, A27, A23, Th20; :: thesis: verum

end;

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;

now :: thesis: for k being Nat st 1 <= k & k <= n - j holds
(((Mx2Tran (Rotation (i,j,n,r))) . p) /^ j) . k = (p /^ j) . k

let k be Nat; :: thesis: ( 1 <= k & k <= n - j implies (((Mx2Tran (Rotation (i,j,n,r))) . p) /^ j) . k = (p /^ j) . k )
assume that
A30: 1 <= k and
A31: k <= n - j ; :: thesis: (((Mx2Tran (Rotation (i,j,n,r))) . p) /^ j) . k = (p /^ j) . k
k in dom (((Mx2Tran (Rotation (i,j,n,r))) . p) /^ j) by A29, A30, A31, FINSEQ_3:25;
then A32: (((Mx2Tran (Rotation (i,j,n,r))) . p) /^ j) . k = ((Mx2Tran (Rotation (i,j,n,r))) . p) . (j + k) by A3, A9, RFINSEQ:def 1;
k in dom (p /^ j) by A16, A30, A31, FINSEQ_3:25;
then A33: (p /^ j) . k = p . (j + k) by A3, A11, RFINSEQ:def 1;
( j + k >= j & j + k <> j ) by A30, NAT_1:11, NAT_1:14;
hence (((Mx2Tran (Rotation (i,j,n,r))) . p) /^ j) . k = (p /^ j) . k by A1, A2, A3, A32, A33, Th20; :: thesis: verum

end;

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