].(- 1),1.[ c= [.(- 1),1.] by XXREAL_1:25;
then A1: ].(- 1),1.[ c= dom arccot by Th24;
for x being Real st x in ].(- 1),1.[ holds
arccot is_differentiable_in x
proof
let x be Real; :: thesis: ( x in ].(- 1),1.[ implies arccot is_differentiable_in x )
A2: dom arccot = rng (cot | ].0,PI.[) by FUNCT_1:33
.= cot .: ].0,PI.[ by RELAT_1:115 ;
assume x in ].(- 1),1.[ ; :: thesis: arccot is_differentiable_in x
then arccot | (dom arccot) is_differentiable_in x by A1, A2, Th72, FDIFF_1:def 6;
hence arccot is_differentiable_in x by RELAT_1:69; :: thesis: verum
end;
hence arccot is_differentiable_on ].(- 1),1.[ by A1, FDIFF_1:9; :: thesis: verum