let a, b be real number ; ( - 1 <= a & a <= 1 & - 1 <= b & b <= 1 implies (1 + (a ^2 )) * (b ^2 ) <= 1 + (b ^2 ) )
assume that
A1:
- 1 <= a
and
A2:
a <= 1
and
A3:
- 1 <= b
and
A4:
b <= 1
; (1 + (a ^2 )) * (b ^2 ) <= 1 + (b ^2 )
(a ^2 ) * (b ^2 ) <= 1
by A1, A2, A3, A4, Th123;
then
(1 * (b ^2 )) + ((a ^2 ) * (b ^2 )) <= 1 + (b ^2 )
by XREAL_1:9;
hence
(1 + (a ^2 )) * (b ^2 ) <= 1 + (b ^2 )
; verum