let x be Real; :: thesis: ( cos x <> 0 implies (sec x) ^2 = 1 + ((tan x) ^2) )
assume cos x <> 0 ; :: thesis: (sec x) ^2 = 1 + ((tan x) ^2)
then A1: (cos x) ^2 <> 0 by SQUARE_1:12;
(sec x) ^2 = (1 ^2) / ((cos x) ^2) by XCMPLX_1:76
.= (((sin x) ^2) + ((cos x) ^2)) / ((cos x) ^2) by SIN_COS:29
.= (((sin x) ^2) / ((cos x) ^2)) + (((cos x) ^2) / ((cos x) ^2)) by XCMPLX_1:62
.= (((sin x) ^2) / ((cos x) ^2)) + 1 by A1, XCMPLX_1:60
.= (((sin x) / (cos x)) ^2) + 1 by XCMPLX_1:76 ;
hence (sec x) ^2 = 1 + ((tan x) ^2) ; :: thesis: verum