let r be Real; :: thesis: for Z being open Subset of REAL
for f being PartFunc of REAL ,REAL st Z c= dom (((- (1 / r)) (#) (arccot * f)) - (id Z)) & ( for x being Real st x in Z holds
( f . x = r * x & r <> 0 & f . x > - 1 & f . x < 1 ) ) holds
( ((- (1 / r)) (#) (arccot * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (1 / r)) (#) (arccot * f)) - (id Z)) `| Z) . x = - (((r * x) ^2 ) / (1 + ((r * x) ^2 ))) ) )
let Z be open Subset of REAL ; :: thesis: for f being PartFunc of REAL ,REAL st Z c= dom (((- (1 / r)) (#) (arccot * f)) - (id Z)) & ( for x being Real st x in Z holds
( f . x = r * x & r <> 0 & f . x > - 1 & f . x < 1 ) ) holds
( ((- (1 / r)) (#) (arccot * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (1 / r)) (#) (arccot * f)) - (id Z)) `| Z) . x = - (((r * x) ^2 ) / (1 + ((r * x) ^2 ))) ) )
let f be PartFunc of REAL ,REAL ; :: thesis: ( Z c= dom (((- (1 / r)) (#) (arccot * f)) - (id Z)) & ( for x being Real st x in Z holds
( f . x = r * x & r <> 0 & f . x > - 1 & f . x < 1 ) ) implies ( ((- (1 / r)) (#) (arccot * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (1 / r)) (#) (arccot * f)) - (id Z)) `| Z) . x = - (((r * x) ^2 ) / (1 + ((r * x) ^2 ))) ) ) )
assume that
A1: Z c= dom (((- (1 / r)) (#) (arccot * f)) - (id Z)) and
A2: for x being Real st x in Z holds
( f . x = r * x & r <> 0 & f . x > - 1 & f . x < 1 ) ; :: thesis: ( ((- (1 / r)) (#) (arccot * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (1 / r)) (#) (arccot * f)) - (id Z)) `| Z) . x = - (((r * x) ^2 ) / (1 + ((r * x) ^2 ))) ) )
A3: for x being Real st x in Z holds
( f . x = (r * x) + 0 & f . x > - 1 & f . x < 1 ) by A2;
Z c= (dom ((- (1 / r)) (#) (arccot * f))) /\ (dom (id Z)) by A1, VALUED_1:12;
then A4: ( Z c= dom ((- (1 / r)) (#) (arccot * f)) & Z c= dom (id Z) ) by XBOOLE_1:18;
then AA: Z c= dom (arccot * f) by VALUED_1:def 5;
then A5: ( arccot * f is_differentiable_on Z & ( for x being Real st x in Z holds
((arccot * f) `| Z) . x = - (r / (1 + (((r * x) + 0 ) ^2 ))) ) ) by A3, Th86;
then A6: ( (- (1 / r)) (#) (arccot * f) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- (1 / r)) (#) (arccot * f)) `| Z) . x = (- (1 / r)) * (diff (arccot * f),x) ) ) by A4, FDIFF_1:28;
AB: for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0 by FUNCT_1:35;
then A7: ( id Z is_differentiable_on Z & ( for x being Real st x in Z holds
((id Z) `| Z) . x = 1 ) ) by A4, FDIFF_1:31;
set g = (- (1 / r)) (#) (arccot * f);
for x being Real st x in Z holds
((((- (1 / r)) (#) (arccot * f)) - (id Z)) `| Z) . x = - (((r * x) ^2 ) / (1 + ((r * x) ^2 )))

proof

let x be Real; :: thesis: ( x in Z implies ((((- (1 / r)) (#) (arccot * f)) - (id Z)) `| Z) . x = - (((r * x) ^2 ) / (1 + ((r * x) ^2 ))) )
assume A8: x in Z ; :: thesis: ((((- (1 / r)) (#) (arccot * f)) - (id Z)) `| Z) . x = - (((r * x) ^2 ) / (1 + ((r * x) ^2 )))
A9: 1 + ((r * x) ^2 ) > 0 by XREAL_1:36, XREAL_1:65;
A10: r <> 0 by A2, A8;
((((- (1 / r)) (#) (arccot * f)) - (id Z)) `| Z) . x = (diff ((- (1 / r)) (#) (arccot * f)),x) - (diff (id Z),x) by A1, A6, A7, A8, FDIFF_1:27
.= ((((- (1 / r)) (#) (arccot * f)) `| Z) . x) - (diff (id Z),x) by A6, A8, FDIFF_1:def 8
.= ((- (1 / r)) * (diff (arccot * f),x)) - (diff (id Z),x) by A4, A5, A8, FDIFF_1:28
.= ((- (1 / r)) * (((arccot * f) `| Z) . x)) - (diff (id Z),x) by A5, A8, FDIFF_1:def 8
.= ((- (1 / r)) * (((arccot * f) `| Z) . x)) - (((id Z) `| Z) . x) by A7, A8, FDIFF_1:def 8
.= ((- (1 / r)) * (- (r / (1 + (((r * x) + 0 ) ^2 ))))) - (((id Z) `| Z) . x) by A3, AA, A8, Th86
.= (((- 1) / r) * ((- r) / (1 + ((r * x) ^2 )))) - 1 by A4, AB, A8, FDIFF_1:31
.= (((- 1) * (- r)) / (r * (1 + ((r * x) ^2 )))) - 1 by XCMPLX_1:77
.= ((1 * r) / (r * (1 + ((r * x) ^2 )))) - 1
.= (1 / (1 + ((r * x) ^2 ))) - 1 by A10, XCMPLX_1:92
.= (1 / (1 + ((r * x) ^2 ))) - ((1 + ((r * x) ^2 )) / (1 + ((r * x) ^2 ))) by A9, XCMPLX_1:60
.= - (((r * x) ^2 ) / (1 + ((r * x) ^2 ))) ;
hence ((((- (1 / r)) (#) (arccot * f)) - (id Z)) `| Z) . x = - (((r * x) ^2 ) / (1 + ((r * x) ^2 ))) ; :: thesis: verum

end;

hence ( ((- (1 / r)) (#) (arccot * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((- (1 / r)) (#) (arccot * f)) - (id Z)) `| Z) . x = - (((r * x) ^2 ) / (1 + ((r * x) ^2 ))) ) ) by A1, A6, A7, FDIFF_1:27; :: thesis: verum