theorem :: SIN_COS9:30

(cot | [.(PI / 4),((3 / 4) * PI).]) * (arccot | [.(- 1),1.]) = id [.(- 1),1.] by Th22, Th26, FUNCT_1:39;