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) (#) (arctan * 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) (#) (arctan * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / r) (#) (arctan * 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) (#) (arctan * 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) (#) (arctan * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / r) (#) (arctan * 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) (#) (arctan * 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) (#) (arctan * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / r) (#) (arctan * f)) - (id Z)) `| Z) . x = - (((r * x) ^2) / (1 + ((r * x) ^2))) ) ) )
assume that
A1: Z c= dom (((1 / r) (#) (arctan * 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) (#) (arctan * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / r) (#) (arctan * 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;
set g = (1 / r) (#) (arctan * f);
A4: for x being Real st x in Z holds
(id Z) . x = (1 * x) + 0 by FUNCT_1:18;
A5: Z c= (dom ((1 / r) (#) (arctan * f))) /\ (dom (id Z)) by A1, VALUED_1:12;
then A6: Z c= dom ((1 / r) (#) (arctan * f)) by XBOOLE_1:18;
A7: Z c= dom (id Z) by A5, XBOOLE_1:18;
then A8: id Z is_differentiable_on Z by A4, FDIFF_1:23;
A9: Z c= dom (arctan * f) by A6, VALUED_1:def 5;
then A10: arctan * f is_differentiable_on Z by A3, Th87;
then A11: (1 / r) (#) (arctan * f) is_differentiable_on Z by A6, FDIFF_1:20;
for x being Real st x in Z holds
((((1 / r) (#) (arctan * f)) - (id Z)) `| Z) . x = - (((r * x) ^2) / (1 + ((r * x) ^2)))

proof

let x be Real; :: thesis: ( x in Z implies ((((1 / r) (#) (arctan * f)) - (id Z)) `| Z) . x = - (((r * x) ^2) / (1 + ((r * x) ^2))) )
A12: 1 + ((r * x) ^2) > 0 by XREAL_1:34, XREAL_1:63;
assume A13: x in Z ; :: thesis: ((((1 / r) (#) (arctan * f)) - (id Z)) `| Z) . x = - (((r * x) ^2) / (1 + ((r * x) ^2)))
then A14: r <> 0 by A2;
((((1 / r) (#) (arctan * f)) - (id Z)) `| Z) . x = (diff (((1 / r) (#) (arctan * f)),x)) - (diff ((id Z),x)) by A1, A11, A8, A13, FDIFF_1:19
.= ((((1 / r) (#) (arctan * f)) `| Z) . x) - (diff ((id Z),x)) by A11, A13, FDIFF_1:def 7
.= ((1 / r) * (diff ((arctan * f),x))) - (diff ((id Z),x)) by A6, A10, A13, FDIFF_1:20
.= ((1 / r) * (((arctan * f) `| Z) . x)) - (diff ((id Z),x)) by A10, A13, FDIFF_1:def 7
.= ((1 / r) * (((arctan * f) `| Z) . x)) - (((id Z) `| Z) . x) by A8, A13, FDIFF_1:def 7
.= ((1 / r) * (r / (1 + (((r * x) + 0) ^2)))) - (((id Z) `| Z) . x) by A3, A9, A13, Th87
.= ((1 / r) * (r / (1 + ((r * x) ^2)))) - 1 by A7, A4, A13, FDIFF_1:23
.= ((1 * r) / (r * (1 + ((r * x) ^2)))) - 1 by XCMPLX_1:76
.= (1 / (1 + ((r * x) ^2))) - 1 by A14, XCMPLX_1:91
.= (1 / (1 + ((r * x) ^2))) - ((1 + ((r * x) ^2)) / (1 + ((r * x) ^2))) by A12, XCMPLX_1:60
.= - (((r * x) ^2) / (1 + ((r * x) ^2))) ;
hence ((((1 / r) (#) (arctan * f)) - (id Z)) `| Z) . x = - (((r * x) ^2) / (1 + ((r * x) ^2))) ; :: thesis: verum

end;

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