A4: sin . (PI / 4) <> 0 by Lm9, COMPTRIG:23;
A5: cot . (PI / 4) = (cos . (PI / 4)) / (sin . (PI / 4)) by Lm9, Th2, RFUNCT_1:def 4
.= 1 by A4, SIN_COS:78, XCMPLX_1:60 ;
cot . ((3 / 4) * PI ) = (cos . ((3 / 4) * PI )) * ((sin . ((3 / 4) * PI )) " ) by Lm10, Th2, RFUNCT_1:def 4
.= (- (sin . (PI / 4))) / (sin . ((PI / 2) + (PI / 4))) by SIN_COS:83
.= (- (sin . (PI / 4))) / (cos . (PI / 4)) by SIN_COS:83
.= - ((sin . (PI / 4)) / (cos . (PI / 4)))
.= - 1 by A4, SIN_COS:78, XCMPLX_1:60 ;
hence ( cot . (PI / 4) = 1 & cot (PI / 4) = 1 & cot . ((3 / 4) * PI ) = - 1 & cot ((3 / 4) * PI ) = - 1 ) by A5, Lm9, Lm10, Th14; :: thesis: verum