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