let s be Real; :: thesis: for i, j, n being Nat
for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n & s ^2 <= ((p . i) ^2) + ((p . j) ^2) holds
ex r being Real st ((Mx2Tran (Rotation (i,j,n,r))) . p) . j = s
let i, j, n be Nat; :: thesis: for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n & s ^2 <= ((p . i) ^2) + ((p . j) ^2) holds
ex r being Real st ((Mx2Tran (Rotation (i,j,n,r))) . p) . j = s
let p be Point of (TOP-REAL n); :: thesis: ( 1 <= i & i < j & j <= n & s ^2 <= ((p . i) ^2) + ((p . j) ^2) implies ex r being Real st ((Mx2Tran (Rotation (i,j,n,r))) . p) . j = s )
set pk = p . i;
set pj = p . j;
set pkj = ((p . i) ^2) + ((p . j) ^2);
set ps = (((p . i) ^2) + ((p . j) ^2)) - (s ^2);
assume that
A1: ( 1 <= i & i < j & j <= n ) and
A2: s ^2 <= ((p . i) ^2) + ((p . j) ^2) ; :: thesis: ex r being Real st ((Mx2Tran (Rotation (i,j,n,r))) . p) . j = s
0 <= s * s by XREAL_1:63;
then A3: (((p . i) ^2) + ((p . j) ^2)) - (s ^2) <= (((p . i) ^2) + ((p . j) ^2)) - 0 by XREAL_1:6;
A4: (s ^2) - (s ^2) <= (((p . i) ^2) + ((p . j) ^2)) - (s ^2) by A2, XREAL_1:6;
then (sqrt ((((p . i) ^2) + ((p . j) ^2)) - (s ^2))) ^2 = (((p . i) ^2) + ((p . j) ^2)) - (s ^2) by SQUARE_1:def 2;
then consider r being Real such that
A5: ((Mx2Tran (Rotation (i,j,n,r))) . p) . i = sqrt ((((p . i) ^2) + ((p . j) ^2)) - (s ^2)) by A1, A3, Th24;
set M = Mx2Tran (Rotation (i,j,n,r));
set Mp = (Mx2Tran (Rotation (i,j,n,r))) . p;
((p . i) ^2) + ((p . j) ^2) = ((sqrt ((((p . i) ^2) + ((p . j) ^2)) - (s ^2))) ^2) + ((((Mx2Tran (Rotation (i,j,n,r))) . p) . j) * (((Mx2Tran (Rotation (i,j,n,r))) . p) . j)) by A5, A1, Lm6
.= ((((p . i) ^2) + ((p . j) ^2)) - (s ^2)) + ((((Mx2Tran (Rotation (i,j,n,r))) . p) . j) * (((Mx2Tran (Rotation (i,j,n,r))) . p) . j)) by A4, SQUARE_1:def 2 ;
then A6: s ^2 = (((Mx2Tran (Rotation (i,j,n,r))) . p) . j) ^2 ;