let x be Real; :: thesis: ( sin (x / 2) <> 0 & cos (x / 2) <> 0 & 1 - ((tan (x / 2)) ^2) <> 0 & not sec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) + 1)) implies sec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) + 1))) )
assume that
A1: sin (x / 2) <> 0 and
A2: cos (x / 2) <> 0 and
A3: 1 - ((tan (x / 2)) ^2) <> 0 ; :: thesis: ( sec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) + 1)) or sec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) + 1))) )
set b = (sec (x / 2)) ^2 ;
set a = 1 - ((tan (x / 2)) ^2);
A4: (1 - ((tan (x / 2)) ^2)) + ((sec (x / 2)) ^2) = (1 + ((tan (x / 2)) ^2)) + (1 - ((tan (x / 2)) ^2)) by A2, Th11
.= 1 + 1 ;
sqrt ((2 * (sec x)) / ((sec x) + 1)) = sqrt ((2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) / ((sec (2 * (x / 2))) + 1)) by A1, A2, Th13
.= sqrt ((2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) / ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) + 1)) by A1, A2, Th13 ;
then A5: sqrt ((2 * (sec x)) / ((sec x) + 1)) = sqrt (((2 * (((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2)))) * (1 - ((tan (x / 2)) ^2))) / (((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) + 1) * (1 - ((tan (x / 2)) ^2)))) by A3, XCMPLX_1:91
.= sqrt ((2 * ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2)))) / (((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2))) + (1 * (1 - ((tan (x / 2)) ^2)))))
.= sqrt ((2 * ((((sec (x / 2)) ^2) / (1 - ((tan (x / 2)) ^2))) * (1 - ((tan (x / 2)) ^2)))) / (((sec (x / 2)) ^2) + (1 - ((tan (x / 2)) ^2)))) by A3, XCMPLX_1:87
.= sqrt ((2 * ((sec (x / 2)) ^2)) / 2) by A3, A4, XCMPLX_1:87
.= |.(sec (x / 2)).| by COMPLEX1:72 ;

per cases ( sec (x / 2) >= 0 or sec (x / 2) < 0 ) ;

suppose sec (x / 2) >= 0 ; :: thesis: ( sec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) + 1)) or sec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) + 1))) )

hence ( sec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) + 1)) or sec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) + 1))) ) by A5, ABSVALUE:def 1; :: thesis: verum

end;

suppose sec (x / 2) < 0 ; :: thesis: ( sec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) + 1)) or sec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) + 1))) )

then (sqrt ((2 * (sec x)) / ((sec x) + 1))) * (- 1) = (- (sec (x / 2))) * (- 1) by A5, ABSVALUE:def 1;
hence ( sec (x / 2) = sqrt ((2 * (sec x)) / ((sec x) + 1)) or sec (x / 2) = - (sqrt ((2 * (sec x)) / ((sec x) + 1))) ) ; :: thesis: verum

end;

end;