let a be non zero Real; :: thesis: for b, r being Real st r = sqrt ((a ^2) + (b ^2)) holds
( r is positive & ((a / r) ^2) + ((b / r) ^2) = 1 )
let b, r be Real; :: thesis: ( r = sqrt ((a ^2) + (b ^2)) implies ( r is positive & ((a / r) ^2) + ((b / r) ^2) = 1 ) )
assume A1: r = sqrt ((a ^2) + (b ^2)) ; :: thesis: ( r is positive & ((a / r) ^2) + ((b / r) ^2) = 1 )
thus r is positive by A1, SQUARE_1:25; :: thesis: ((a / r) ^2) + ((b / r) ^2) = 1
reconsider r = r as positive Real by A1, SQUARE_1:25;
( (a / r) ^2 = (a ^2) / (r ^2) & (b / r) ^2 = (b ^2) / (r ^2) ) by XCMPLX_1:76;
then ((a / r) ^2) + ((b / r) ^2) = ((a ^2) + (b ^2)) / (r ^2)
.= (r ^2) / (r ^2) by A1, SQUARE_1:def 2
.= 1 by XCMPLX_1:60 ;
hence ((a / r) ^2) + ((b / r) ^2) = 1 ; :: thesis: verum