let x be Real; :: 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:8;
then ((x ^2) - 1) * ((x ^2) - 1) > 0 * ((x ^2) - 1) ;
then A1: ( x ^2 >= 0 & ((((x ^2) ^2) - (2 * (x ^2))) + 1) + (4 * (x ^2)) > 0 + (4 * (x ^2)) ) by XREAL_1:8, XREAL_1:63;
((2 * x) / (1 + (x ^2))) ^2 = ((2 * x) ^2) / ((1 + (x ^2)) ^2) by XCMPLX_1:76
.= (4 * (x ^2)) / ((((x ^2) ^2) + (2 * (x ^2))) + 1) ;
hence ((2 * x) / (1 + (x ^2))) ^2 < 1 by A1, XREAL_1:189; :: thesis: verum