let x, y be Real; :: thesis: ( |.x.| < 1 & |.y.| < 1 implies |.((x + y) / (1 + (x * y))).| <= 1 )
assume that
A1: |.x.| < 1 and
A2: |.y.| < 1 ; :: thesis: |.((x + y) / (1 + (x * y))).| <= 1

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

suppose A3: 1 + (x * y) <> 0 ; :: thesis: |.((x + y) / (1 + (x * y))).| <= 1

y ^2 < 1 by A2, Lm7;
then A4: (y ^2) - (y ^2) < 1 - (y ^2) by XREAL_1:14;
x ^2 < 1 by A1, Lm7;
then (x ^2) - (x ^2) < 1 - (x ^2) by XREAL_1:14;
then 0 < (1 - (x ^2)) * (1 - (y ^2)) by A4;
then 0 + ((x ^2) + (y ^2)) < (((1 - (y ^2)) - (x ^2)) + ((x ^2) * (y ^2))) + ((x ^2) + (y ^2)) by XREAL_1:8;
then A5: ((x ^2) + (y ^2)) + ((2 * x) * y) < (1 + ((x ^2) * (y ^2))) + ((2 * x) * y) by XREAL_1:8;
(1 + (x * y)) ^2 > 0 by A3, SQUARE_1:12;
then ((x + y) ^2) / ((1 + (x * y)) ^2) < (((x * y) + 1) ^2) / ((1 + (x * y)) ^2) by A5, XREAL_1:74;
then ((x + y) ^2) / ((1 + (x * y)) ^2) < 1 by A3, XCMPLX_1:60;
then ((x + y) / (1 + (x * y))) ^2 < 1 by XCMPLX_1:76;
hence |.((x + y) / (1 + (x * y))).| <= 1 by Lm8; :: thesis: verum

end;

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

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

end;

end;