let a, b be Real; :: thesis: ( not a ^2 = 1 / b or a = 1 / (sqrt b) or a = (- 1) / (sqrt b) )
assume A1: a ^2 = 1 / b ; :: thesis: ( a = 1 / (sqrt b) or a = (- 1) / (sqrt b) )
reconsider ib = 1 / b as Real ;
A2: 0 <= b by A1, Th07;
0 <= ib by A1, Th07;
then ib = (sqrt (1 / b)) ^2 by SQUARE_1:def 2;
then A3: ( a = sqrt (1 / b) or a = - (sqrt (1 / b)) ) by A1, SQUARE_1:40;
- ((sqrt 1) / (sqrt b)) = (- 1) / (sqrt b) by XCMPLX_1:187, SQUARE_1:18;
hence ( a = 1 / (sqrt b) or a = (- 1) / (sqrt b) ) by A3, A2, SQUARE_1:30, SQUARE_1:18; :: thesis: verum