let x be Real; :: 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:12;
(cosec x) ^2 = (1 ^2) / ((sin x) ^2) by XCMPLX_1:76
.= (((sin x) ^2) + ((cos x) ^2)) / ((sin x) ^2) by SIN_COS:29
.= (((sin x) ^2) / ((sin x) ^2)) + (((cos x) ^2) / ((sin x) ^2)) by XCMPLX_1:62
.= 1 + (((cos x) ^2) / ((sin x) ^2)) by A1, XCMPLX_1:60
.= 1 + (((cos x) / (sin x)) ^2) by XCMPLX_1:76 ;
hence (cosec x) ^2 = 1 + ((cot x) ^2) ; :: thesis: verum