let Z be open Subset of REAL; for g being PartFunc of REAL,REAL st not 0 in Z & Z c= dom (g (#) (arctan * ((id Z) ^))) & g = #Z 2 & ( for x being Real st x in Z holds
( ((id Z) ^) . x > - 1 & ((id Z) ^) . x < 1 ) ) holds
( g (#) (arctan * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (arctan * ((id Z) ^))) `| Z) . x = ((2 * x) * (arctan . (1 / x))) - ((x ^2) / (1 + (x ^2))) ) )
let g be PartFunc of REAL,REAL; ( not 0 in Z & Z c= dom (g (#) (arctan * ((id Z) ^))) & g = #Z 2 & ( for x being Real st x in Z holds
( ((id Z) ^) . x > - 1 & ((id Z) ^) . x < 1 ) ) implies ( g (#) (arctan * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (arctan * ((id Z) ^))) `| Z) . x = ((2 * x) * (arctan . (1 / x))) - ((x ^2) / (1 + (x ^2))) ) ) )
set f = id Z;
assume that
A1:
not 0 in Z
and
A2:
Z c= dom (g (#) (arctan * ((id Z) ^)))
and
A3:
g = #Z 2
and
A4:
for x being Real st x in Z holds
( ((id Z) ^) . x > - 1 & ((id Z) ^) . x < 1 )
; ( g (#) (arctan * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (arctan * ((id Z) ^))) `| Z) . x = ((2 * x) * (arctan . (1 / x))) - ((x ^2) / (1 + (x ^2))) ) )
A5:
for x being Real st x in Z holds
g is_differentiable_in x
by A3, TAYLOR_1:2;
A6:
Z c= (dom g) /\ (dom (arctan * ((id Z) ^)))
by A2, VALUED_1:def 4;
then A7:
Z c= dom (arctan * ((id Z) ^))
by XBOOLE_1:18;
then A8:
arctan * ((id Z) ^) is_differentiable_on Z
by A1, A4, SIN_COS9:111;
Z c= dom g
by A6, XBOOLE_1:18;
then A9:
g is_differentiable_on Z
by A5, FDIFF_1:9;
A10:
for x being Real st x in Z holds
(g `| Z) . x = 2 * x
for y being object st y in Z holds
y in dom ((id Z) ^)
by A7, FUNCT_1:11;
then A11:
Z c= dom ((id Z) ^)
by TARSKI:def 3;
for x being Real st x in Z holds
((g (#) (arctan * ((id Z) ^))) `| Z) . x = ((2 * x) * (arctan . (1 / x))) - ((x ^2) / (1 + (x ^2)))
proof
let x be
Real;
( x in Z implies ((g (#) (arctan * ((id Z) ^))) `| Z) . x = ((2 * x) * (arctan . (1 / x))) - ((x ^2) / (1 + (x ^2))) )
assume A12:
x in Z
;
((g (#) (arctan * ((id Z) ^))) `| Z) . x = ((2 * x) * (arctan . (1 / x))) - ((x ^2) / (1 + (x ^2)))
then ((g (#) (arctan * ((id Z) ^))) `| Z) . x =
(((arctan * ((id Z) ^)) . x) * (diff (g,x))) + ((g . x) * (diff ((arctan * ((id Z) ^)),x)))
by A2, A8, A9, FDIFF_1:21
.=
(((arctan * ((id Z) ^)) . x) * ((g `| Z) . x)) + ((g . x) * (diff ((arctan * ((id Z) ^)),x)))
by A9, A12, FDIFF_1:def 7
.=
(((arctan * ((id Z) ^)) . x) * (2 * x)) + ((g . x) * (diff ((arctan * ((id Z) ^)),x)))
by A10, A12
.=
(((arctan * ((id Z) ^)) . x) * (2 * x)) + ((x #Z 2) * (diff ((arctan * ((id Z) ^)),x)))
by A3, TAYLOR_1:def 1
.=
(((arctan * ((id Z) ^)) . x) * (2 * x)) + ((x #Z 2) * (((arctan * ((id Z) ^)) `| Z) . x))
by A8, A12, FDIFF_1:def 7
.=
(((arctan * ((id Z) ^)) . x) * (2 * x)) + ((x #Z (1 + 1)) * (- (1 / (1 + (x ^2)))))
by A1, A4, A7, A12, SIN_COS9:111
.=
(((arctan * ((id Z) ^)) . x) * (2 * x)) + (((x #Z 1) * (x #Z 1)) * (- (1 / (1 + (x ^2)))))
by TAYLOR_1:1
.=
(((arctan * ((id Z) ^)) . x) * (2 * x)) + ((x * (x #Z 1)) * (- (1 / (1 + (x ^2)))))
by PREPOWER:35
.=
(((arctan * ((id Z) ^)) . x) * (2 * x)) + ((x ^2) * (- (1 / (1 + (x ^2)))))
by PREPOWER:35
.=
((arctan . (((id Z) ^) . x)) * (2 * x)) - ((x ^2) / (1 + (x ^2)))
by A7, A12, FUNCT_1:12
.=
((arctan . (((id Z) . x) ")) * (2 * x)) - ((x ^2) / (1 + (x ^2)))
by A11, A12, RFUNCT_1:def 2
.=
((2 * x) * (arctan . (1 / x))) - ((x ^2) / (1 + (x ^2)))
by A12, FUNCT_1:18
;
hence
((g (#) (arctan * ((id Z) ^))) `| Z) . x = ((2 * x) * (arctan . (1 / x))) - ((x ^2) / (1 + (x ^2)))
;
verum
end;
hence
( g (#) (arctan * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (arctan * ((id Z) ^))) `| Z) . x = ((2 * x) * (arctan . (1 / x))) - ((x ^2) / (1 + (x ^2))) ) )
by A2, A8, A9, FDIFF_1:21; verum