let a, b be Real; :: thesis: ( (a ^2) + (b ^2) = 1 & a = 0 & not b = 1 implies b = - 1 )
assume that
A1: (a ^2) + (b ^2) = 1 and
A2: a = 0 ; :: thesis: ( b = 1 or b = - 1 )
b ^2 = 1 ^2 by A1, A2;
hence ( b = 1 or b = - 1 ) by SQUARE_1:40; :: thesis: verum