let x be real number ; :: thesis: ( x ^2 < 1 implies ((2 * x) / (1 + (x ^2 ))) ^2 < 1 )
assume x ^2 < 1 ; :: thesis: ((2 * x) / (1 + (x ^2 ))) ^2 < 1
then (x ^2 ) + (- 1) < 1 + (- 1) by XREAL_1:10;
then ((x ^2 ) - 1) * ((x ^2 ) - 1) > 0 * ((x ^2 ) - 1) by XREAL_1:71;
then A1: ( x ^2 >= 0 & ((((x ^2 ) ^2 ) - (2 * (x ^2 ))) + 1) + (4 * (x ^2 )) > 0 + (4 * (x ^2 )) ) by XREAL_1:10, XREAL_1:65;
((2 * x) / (1 + (x ^2 ))) ^2 = ((2 * x) ^2 ) / ((1 + (x ^2 )) ^2 ) by XCMPLX_1:77
.= (4 * (x ^2 )) / ((((x ^2 ) ^2 ) + (2 * (x ^2 ))) + 1) ;
hence ((2 * x) / (1 + (x ^2 ))) ^2 < 1 by A1, XREAL_1:191; :: thesis: verum