let a, b be Real; :: thesis: ( not ((a * b) ^2) + (b ^2) = 1 or b = 1 / (sqrt (1 + (a ^2))) or b = (- 1) / (sqrt (1 + (a ^2))) )
assume a1: ((a * b) ^2) + (b ^2) = 1 ; :: thesis: ( b = 1 / (sqrt (1 + (a ^2))) or b = (- 1) / (sqrt (1 + (a ^2))) )
b ^2 = (((a ^2) + 1) * (b ^2)) / ((a ^2) + 1) by XCMPLX_1:89, Lem03
.= 1 / ((a ^2) + 1) by a1 ;
hence ( b = 1 / (sqrt (1 + (a ^2))) or b = (- 1) / (sqrt (1 + (a ^2))) ) by Lem04; :: thesis: verum