let a, b be Real; ( 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
; ( 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; verum