let a, b be Real; :: thesis: ( a <> 0 & - 1 < a & a < 1 & b = (2 + (sqrt (delta ((a * a),(- 2),1)))) / ((2 * a) * a) implies (((((1 + (a * a)) * b) * b) - (2 * b)) + 1) - (b * b) = 0 )
assume that
A1: a <> 0 and
A2: ( - 1 < a & a < 1 ) and
A3: b = (2 + (sqrt (delta ((a * a),(- 2),1)))) / ((2 * a) * a) ; :: thesis: (((((1 + (a * a)) * b) * b) - (2 * b)) + 1) - (b * b) = 0
set x1 = ((- (- 2)) - (sqrt (delta ((a * a),(- 2),1)))) / (2 * (a * a));
set x2 = ((- (- 2)) + (sqrt (delta ((a * a),(- 2),1)))) / (2 * (a * a));
A4: 0 <= 1 - (a ^2)

proof

(a ^2) * (1 ^2) <= 1 by A2, SQUARE_1:53;
then a ^2 < 1 by A2, SQUARE_1:41, XXREAL_0:1;
then (a ^2) - (a ^2) < 1 - (a ^2) by XREAL_1:9;
hence 0 <= 1 - (a ^2) ; :: thesis: verum

end;

delta ((a * a),(- 2),1) >= 0

proof

delta ((a * a),(- 2),1) = ((- 2) ^2) - ((4 * (a * a)) * 1) by QUIN_1:def 1
.= 4 * (1 - (a ^2)) ;
hence delta ((a * a),(- 2),1) >= 0 by A4; :: thesis: verum

end;

then (((a * a) * (b ^2)) + ((- 2) * b)) + 1 = ((a * a) * (b - (((- (- 2)) - (sqrt (delta ((a * a),(- 2),1)))) / (2 * (a * a))))) * ((((- (- 2)) + (sqrt (delta ((a * a),(- 2),1)))) / (2 * (a * a))) - (((- (- 2)) + (sqrt (delta ((a * a),(- 2),1)))) / (2 * (a * a)))) by A3, A1, QUIN_1:16
.= 0 ;
hence (((((1 + (a * a)) * b) * b) - (2 * b)) + 1) - (b * b) = 0 ; :: thesis: verum