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) . i = 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) . i = 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) . i = s )
set pk = p . i;
set pj = p . j;
set pkj = ((p . i) ^2) + ((p . j) ^2);
set P = sqrt (((p . i) ^2) + ((p . j) ^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) . i = s
A3: ( 0 <= (p . i) * (p . i) & 0 <= (p . j) * (p . j) ) by XREAL_1:63;

per cases ( p . i <> 0 or p . j <> 0 or ( p . i = 0 & p . j = 0 ) ) ;

suppose A4: ( p . i <> 0 or p . j <> 0 ) ; :: thesis: ex r being Real st ((Mx2Tran (Rotation (i,j,n,r))) . p) . i = s

A5: 0 <= (p . i) * (p . i) by XREAL_1:63;
A6: sqrt (((p . i) ^2) + ((p . j) ^2)) > 0 by A3, A4, SQUARE_1:25;
then A7: (s / (sqrt (((p . i) ^2) + ((p . j) ^2)))) * (sqrt (((p . i) ^2) + ((p . j) ^2))) = s by XCMPLX_1:87;
A8: 0 <= (p . j) * (p . j) by XREAL_1:63;
then ((p . i) ^2) + 0 <= ((p . i) ^2) + ((p . j) ^2) by XREAL_1:6;
then A9: sqrt ((p . i) ^2) <= sqrt (((p . i) ^2) + ((p . j) ^2)) by A5, SQUARE_1:26;

now :: thesis: (p . i) / (sqrt (((p . i) ^2) + ((p . j) ^2))) in [.(- 1),1.]

per cases ( p . i >= 0 or p . i <= 0 ) ;

suppose A10: p . i >= 0 ; :: thesis: (p . i) / (sqrt (((p . i) ^2) + ((p . j) ^2))) in [.(- 1),1.]

then A11: p . i <= sqrt (((p . i) ^2) + ((p . j) ^2)) by A9, SQUARE_1:22;
then (p . i) / (sqrt (((p . i) ^2) + ((p . j) ^2))) <= 1 by A6, XREAL_1:185;
hence (p . i) / (sqrt (((p . i) ^2) + ((p . j) ^2))) in [.(- 1),1.] by A10, A11, XXREAL_1:1; :: thesis: verum

end;

suppose A12: p . i <= 0 ; :: thesis: (p . i) / (sqrt (((p . i) ^2) + ((p . j) ^2))) in [.(- 1),1.]

then - (p . i) <= sqrt (((p . i) ^2) + ((p . j) ^2)) by A9, SQUARE_1:23;
then - 1 <= (p . i) / (sqrt (((p . i) ^2) + ((p . j) ^2))) by A6, XREAL_1:194;
hence (p . i) / (sqrt (((p . i) ^2) + ((p . j) ^2))) in [.(- 1),1.] by A6, A12, XXREAL_1:1; :: thesis: verum

end;

end;

end;

then consider x being object such that
A13: x in dom sin and
x in [.(- (PI / 2)),(PI / 2).] and
A14: sin . x = (p . i) / (sqrt (((p . i) ^2) + ((p . j) ^2))) by FUNCT_1:def 6, SIN_COS6:45;
A15: (sqrt (((p . i) ^2) + ((p . j) ^2))) * (sqrt (((p . i) ^2) + ((p . j) ^2))) = (sqrt (((p . i) ^2) + ((p . j) ^2))) ^2
.= ((p . i) ^2) + ((p . j) ^2) by A5, A8, SQUARE_1:def 2 ;
0 <= s * s by XREAL_1:63;
then A16: sqrt (s ^2) <= sqrt (((p . i) ^2) + ((p . j) ^2)) by A2, SQUARE_1:26;

now :: thesis: s / (sqrt (((p . i) ^2) + ((p . j) ^2))) in [.(- 1),1.]

per cases ( s >= 0 or s <= 0 ) ;

suppose A17: s >= 0 ; :: thesis: s / (sqrt (((p . i) ^2) + ((p . j) ^2))) in [.(- 1),1.]

then A18: s <= sqrt (((p . i) ^2) + ((p . j) ^2)) by A16, SQUARE_1:22;
then s / (sqrt (((p . i) ^2) + ((p . j) ^2))) <= 1 by A6, XREAL_1:185;
hence s / (sqrt (((p . i) ^2) + ((p . j) ^2))) in [.(- 1),1.] by A17, A18, XXREAL_1:1; :: thesis: verum

end;

suppose A19: s <= 0 ; :: thesis: s / (sqrt (((p . i) ^2) + ((p . j) ^2))) in [.(- 1),1.]

then - s <= sqrt (((p . i) ^2) + ((p . j) ^2)) by A16, SQUARE_1:23;
then - 1 <= s / (sqrt (((p . i) ^2) + ((p . j) ^2))) by A6, XREAL_1:194;
hence s / (sqrt (((p . i) ^2) + ((p . j) ^2))) in [.(- 1),1.] by A6, A19, XXREAL_1:1; :: thesis: verum

end;

end;

end;

then consider y being object such that
y in dom sin and
A20: y in [.(- (PI / 2)),(PI / 2).] and
A21: sin . y = s / (sqrt (((p . i) ^2) + ((p . j) ^2))) by FUNCT_1:def 6, SIN_COS6:45;
reconsider y = y as Real by A20;
A22: ((sqrt (((p . i) ^2) + ((p . j) ^2))) * (p . i)) / (sqrt (((p . i) ^2) + ((p . j) ^2))) = p . i by A6, XCMPLX_1:89;
reconsider x = x as Element of REAL by A13, FUNCT_2:def 1;
A23: sin . x = sin x by SIN_COS:def 17;
((p . i) / (sqrt (((p . i) ^2) + ((p . j) ^2)))) * ((p . i) / (sqrt (((p . i) ^2) + ((p . j) ^2)))) = ((p . i) * (p . i)) / (((p . i) ^2) + ((p . j) ^2)) by A15, XCMPLX_1:76;
then ((cos x) * (cos x)) + (((p . i) * (p . i)) / (((p . i) ^2) + ((p . j) ^2))) = 1 by A14, A23, SIN_COS:29;
then (cos x) * (cos x) = 1 - (((p . i) * (p . i)) / (((p . i) ^2) + ((p . j) ^2)))
.= ((((p . i) ^2) + ((p . j) ^2)) / (((p . i) ^2) + ((p . j) ^2))) - (((p . i) * (p . i)) / (((p . i) ^2) + ((p . j) ^2))) by A3, A4, XCMPLX_1:60
.= ((p . j) * (p . j)) / (((p . i) ^2) + ((p . j) ^2))
.= ((p . j) / (sqrt (((p . i) ^2) + ((p . j) ^2)))) ^2 by A15, XCMPLX_1:76 ;
then A24: (cos x) ^2 = ((p . j) / (sqrt (((p . i) ^2) + ((p . j) ^2)))) ^2 ;

per cases ( cos x = (p . j) / (sqrt (((p . i) ^2) + ((p . j) ^2))) or cos x = - ((p . j) / (sqrt (((p . i) ^2) + ((p . j) ^2)))) ) by A24, SQUARE_1:40;

suppose A25: cos x = (p . j) / (sqrt (((p . i) ^2) + ((p . j) ^2))) ; :: thesis: ex r being Real st ((Mx2Tran (Rotation (i,j,n,r))) . p) . i = s

take r = x - y; :: thesis: ((Mx2Tran (Rotation (i,j,n,r))) . p) . i = s
- (sin y) = sin ((- x) + r) by SIN_COS:31
.= ((sin (- x)) * (cos r)) + ((cos (- x)) * (sin r)) by SIN_COS:75
.= ((- (sin x)) * (cos r)) + ((cos (- x)) * (sin r)) by SIN_COS:31
.= (- ((sin x) * (cos r))) + ((cos x) * (sin r)) by SIN_COS:31
.= (- ((sin x) * (cos r))) + (- ((cos x) * (- (sin r)))) ;
then sin y = ((sin x) * (cos r)) + ((cos x) * (- (sin r))) ;
hence s = (sqrt (((p . i) ^2) + ((p . j) ^2))) * ((((p . i) / (sqrt (((p . i) ^2) + ((p . j) ^2)))) * (cos r)) + (((p . j) / (sqrt (((p . i) ^2) + ((p . j) ^2)))) * (- (sin r)))) by A7, A14, A21, A23, A25, SIN_COS:def 17
.= ((((sqrt (((p . i) ^2) + ((p . j) ^2))) * (p . i)) / (sqrt (((p . i) ^2) + ((p . j) ^2)))) * (cos r)) + ((((sqrt (((p . i) ^2) + ((p . j) ^2))) * (p . j)) / (sqrt (((p . i) ^2) + ((p . j) ^2)))) * (- (sin r)))
.= ((p . i) * (cos r)) + ((p . j) * (- (sin r))) by A6, A22, XCMPLX_1:89
.= ((Mx2Tran (Rotation (i,j,n,r))) . p) . i by A1, Th21 ;
:: thesis: verum

end;

suppose A26: cos x = - ((p . j) / (sqrt (((p . i) ^2) + ((p . j) ^2)))) ; :: thesis: ex r being Real st ((Mx2Tran (Rotation (i,j,n,r))) . p) . i = s

take r = y - x; :: thesis: ((Mx2Tran (Rotation (i,j,n,r))) . p) . i = s
sin y = sin (x + r)
.= ((sin x) * (cos r)) + ((cos x) * (sin r)) by SIN_COS:75
.= (((p . i) / (sqrt (((p . i) ^2) + ((p . j) ^2)))) * (cos r)) + (((p . j) / (sqrt (((p . i) ^2) + ((p . j) ^2)))) * (- (sin r))) by A14, A26, SIN_COS:def 17 ;
hence s = (sqrt (((p . i) ^2) + ((p . j) ^2))) * ((((p . i) / (sqrt (((p . i) ^2) + ((p . j) ^2)))) * (cos r)) + (((p . j) / (sqrt (((p . i) ^2) + ((p . j) ^2)))) * (- (sin r)))) by A7, A21, SIN_COS:def 17
.= ((((sqrt (((p . i) ^2) + ((p . j) ^2))) * (p . i)) / (sqrt (((p . i) ^2) + ((p . j) ^2)))) * (cos r)) + ((((sqrt (((p . i) ^2) + ((p . j) ^2))) * (p . j)) / (sqrt (((p . i) ^2) + ((p . j) ^2)))) * (- (sin r)))
.= ((p . i) * (cos r)) + ((p . j) * (- (sin r))) by A6, A22, XCMPLX_1:89
.= ((Mx2Tran (Rotation (i,j,n,r))) . p) . i by A1, Th21 ;
:: thesis: verum

end;

end;

end;

suppose A27: ( p . i = 0 & p . j = 0 ) ; :: thesis: ex r being Real st ((Mx2Tran (Rotation (i,j,n,r))) . p) . i = s

take r = 0 ; :: thesis: ((Mx2Tran (Rotation (i,j,n,r))) . p) . i = s
set M = Mx2Tran (Rotation (i,j,n,r));
Mx2Tran (Rotation (i,j,n,r)) = Mx2Tran (1. (F_Real,n)) by A1, Th18;
then A28: Mx2Tran (Rotation (i,j,n,r)) = id (TOP-REAL n) by MATRTOP1:33;
s = 0 by A2, A27, XREAL_1:63;
hence ((Mx2Tran (Rotation (i,j,n,r))) . p) . i = s by A27, A28; :: thesis: verum

end;

end;