let x be real number ; :: thesis: ( sin x <> 0 implies (cosec x) ^2 = 1 + ((cot x) ^2 ) )
assume sin x <> 0 ; :: thesis: (cosec x) ^2 = 1 + ((cot x) ^2 )
then A1: (sin x) ^2 <> 0 by SQUARE_1:74;
(cosec x) ^2 = (1 ^2 ) / ((sin x) ^2 ) by XCMPLX_1:77
.= (((sin x) ^2 ) + ((cos x) ^2 )) / ((sin x) ^2 ) by SIN_COS:32
.= (((sin x) ^2 ) / ((sin x) ^2 )) + (((cos x) ^2 ) / ((sin x) ^2 )) by XCMPLX_1:63
.= 1 + (((cos x) ^2 ) / ((sin x) ^2 )) by A1, XCMPLX_1:60
.= 1 + (((cos x) / (sin x)) ^2 ) by XCMPLX_1:77 ;
hence (cosec x) ^2 = 1 + ((cot x) ^2 ) ; :: thesis: verum