let x, y be real number ; :: thesis: ( abs x < 1 & abs y < 1 implies abs ((x + y) / (1 + (x * y))) <= 1 )
assume A1: ( abs x < 1 & abs y < 1 ) ; :: thesis: abs ((x + y) / (1 + (x * y))) <= 1

per cases ( 1 + (x * y) <> 0 or 1 + (x * y) = 0 ) ;

suppose A2: 1 + (x * y) <> 0 ; :: thesis: abs ((x + y) / (1 + (x * y))) <= 1

( x ^2 < 1 & y ^2 < 1 ) by A1, Lm7;
then ( (x ^2 ) - (x ^2 ) < 1 - (x ^2 ) & (y ^2 ) - (y ^2 ) < 1 - (y ^2 ) ) by XREAL_1:16;
then 0 < (1 - (x ^2 )) * (1 - (y ^2 )) ;
then 0 + ((x ^2 ) + (y ^2 )) < (((1 - (y ^2 )) - (x ^2 )) + ((x ^2 ) * (y ^2 ))) + ((x ^2 ) + (y ^2 )) by XREAL_1:10;
then A3: ((x ^2 ) + (y ^2 )) + ((2 * x) * y) < (1 + ((x ^2 ) * (y ^2 ))) + ((2 * x) * y) by XREAL_1:10;
A4: (1 + (x * y)) ^2 > 0 by A2, SQUARE_1:74;
then ((x + y) ^2 ) / ((1 + (x * y)) ^2 ) < (((x * y) + 1) ^2 ) / ((1 + (x * y)) ^2 ) by A3, XREAL_1:76;
then ((x + y) ^2 ) / ((1 + (x * y)) ^2 ) < 1 by A4, XCMPLX_1:60;
then ((x + y) / (1 + (x * y))) ^2 < 1 by XCMPLX_1:77;
hence abs ((x + y) / (1 + (x * y))) <= 1 by Lm8; :: thesis: verum

end;

suppose 1 + (x * y) = 0 ; :: thesis: abs ((x + y) / (1 + (x * y))) <= 1

then abs ((x + y) / (1 + (x * y))) = abs 0 by XCMPLX_1:49
.= 0 by ABSVALUE:7 ;
hence abs ((x + y) / (1 + (x * y))) <= 1 ; :: thesis: verum

end;

end;