let a be Real; :: thesis: ( - 1 < a & a < 1 implies ex b being Real st (((((1 + (a * a)) * b) * b) - (2 * b)) + 1) - (b * b) = 0 )
assume A1: ( - 1 < a & a < 1 ) ; :: thesis: ex b being Real st (((((1 + (a * a)) * b) * b) - (2 * b)) + 1) - (b * b) = 0
per cases ( a = 0 or a <> 0 ) ;
suppose A2: a = 0 ; :: thesis: ex b being Real st (((((1 + (a * a)) * b) * b) - (2 * b)) + 1) - (b * b) = 0
set b = 1 / 2;
take 1 / 2 ; :: thesis: (((((1 + (a * a)) * (1 / 2)) * (1 / 2)) - (2 * (1 / 2))) + 1) - ((1 / 2) * (1 / 2)) = 0
thus (((((1 + (a * a)) * (1 / 2)) * (1 / 2)) - (2 * (1 / 2))) + 1) - ((1 / 2) * (1 / 2)) = 0 by A2; :: thesis: verum
end;
suppose A3: a <> 0 ; :: thesis: ex b being Real st (((((1 + (a * a)) * b) * b) - (2 * b)) + 1) - (b * b) = 0
take b = (2 + (sqrt (delta ((a * a),(- 2),1)))) / ((2 * a) * a); :: thesis: (((((1 + (a * a)) * b) * b) - (2 * b)) + 1) - (b * b) = 0
thus (((((1 + (a * a)) * b) * b) - (2 * b)) + 1) - (b * b) = 0 by A1, A3, Th13; :: thesis: verum
end;
end;