let r be real number ; :: 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) . i) * (((Mx2Tran (Rotation (i,j,n,r))) . p) . i)) + ((((Mx2Tran (Rotation (i,j,n,r))) . p) . j) * (((Mx2Tran (Rotation (i,j,n,r))) . p) . j)) = ((p . i) * (p . i)) + ((p . j) * (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) . i) * (((Mx2Tran (Rotation (i,j,n,r))) . p) . i)) + ((((Mx2Tran (Rotation (i,j,n,r))) . p) . j) * (((Mx2Tran (Rotation (i,j,n,r))) . p) . j)) = ((p . i) * (p . i)) + ((p . j) * (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) . i) * (((Mx2Tran (Rotation (i,j,n,r))) . p) . i)) + ((((Mx2Tran (Rotation (i,j,n,r))) . p) . j) * (((Mx2Tran (Rotation (i,j,n,r))) . p) . j)) = ((p . i) * (p . i)) + ((p . j) * (p . j)) )
set pk = p . i;
set pj = p . j;
set pkj = ((p . i) ^2) + ((p . j) ^2);
set M = Mx2Tran (Rotation (i,j,n,r));
set S = sin r;
set C = cos r;
set Mp = (Mx2Tran (Rotation (i,j,n,r))) . p;
A1: ((cos r) * (cos r)) + ((sin r) * (sin r)) = 1 by SIN_COS:29;
assume A2: ( 1 <= i & i < j & j <= n ) ; :: thesis: ((((Mx2Tran (Rotation (i,j,n,r))) . p) . i) * (((Mx2Tran (Rotation (i,j,n,r))) . p) . i)) + ((((Mx2Tran (Rotation (i,j,n,r))) . p) . j) * (((Mx2Tran (Rotation (i,j,n,r))) . p) . j)) = ((p . i) * (p . i)) + ((p . j) * (p . j))
then ((Mx2Tran (Rotation (i,j,n,r))) . p) . i = ((p . i) * (cos r)) + ((p . j) * (- (sin r))) by Th19;
then A3: (((Mx2Tran (Rotation (i,j,n,r))) . p) . i) * (((Mx2Tran (Rotation (i,j,n,r))) . p) . i) = (((((p . i) * (p . i)) * (cos r)) * (cos r)) - ((((2 * (p . i)) * (p . j)) * (cos r)) * (sin r))) + ((((p . j) * (p . j)) * (sin r)) * (sin r)) ;
((Mx2Tran (Rotation (i,j,n,r))) . p) . j = ((p . i) * (sin r)) + ((p . j) * (cos r)) by A2, Th20;
then (((Mx2Tran (Rotation (i,j,n,r))) . p) . j) * (((Mx2Tran (Rotation (i,j,n,r))) . p) . j) = (((((p . i) * (p . i)) * (sin r)) * (sin r)) + ((2 * ((p . i) * (p . j))) * ((cos r) * (sin r)))) + (((p . j) * (p . j)) * ((cos r) * (cos r))) ;
hence ((((Mx2Tran (Rotation (i,j,n,r))) . p) . i) * (((Mx2Tran (Rotation (i,j,n,r))) . p) . i)) + ((((Mx2Tran (Rotation (i,j,n,r))) . p) . j) * (((Mx2Tran (Rotation (i,j,n,r))) . p) . j)) = (((p . i) * (p . i)) * (((cos r) * (cos r)) + ((sin r) * (sin r)))) + (((p . j) * (p . j)) * (((cos r) * (cos r)) + ((sin r) * (sin r)))) by A3
.= ((p . i) * (p . i)) + ((p . j) * (p . j)) by A1 ;
:: thesis: verum