let Z be open Subset of REAL ; :: thesis: for f1, f2 being PartFunc of REAL ,REAL st Z c= dom ((1 / 2) (#) (ln * (f1 + f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds
f1 . x = 1 ) holds
( (1 / 2) (#) (ln * (f1 + f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (1 + (x ^2 )) ) )
let f1, f2 be PartFunc of REAL ,REAL ; :: thesis: ( Z c= dom ((1 / 2) (#) (ln * (f1 + f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds
f1 . x = 1 ) implies ( (1 / 2) (#) (ln * (f1 + f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (1 + (x ^2 )) ) ) )
assume that
A1: Z c= dom ((1 / 2) (#) (ln * (f1 + f2))) and
A2: f2 = #Z 2 and
A3: for x being Real st x in Z holds
f1 . x = 1 ; :: thesis: ( (1 / 2) (#) (ln * (f1 + f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (1 + (x ^2 )) ) )
A4: Z c= dom (ln * (f1 + f2)) by A1, VALUED_1:def 5;
then for y being set st y in Z holds
y in dom (f1 + f2) by FUNCT_1:21;
then A5: Z c= dom (f1 + f2) by TARSKI:def 3;
A6: ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + f2) `| Z) . x = 2 * x ) ) by A2, A3, A5, Th99;
for x being Real st x in Z holds
ln * (f1 + f2) is_differentiable_in x

proof

let x be Real; :: thesis: ( x in Z implies ln * (f1 + f2) is_differentiable_in x )
assume A8: x in Z ; :: thesis: ln * (f1 + f2) is_differentiable_in x
then A9: f1 + f2 is_differentiable_in x by A6, FDIFF_1:16;
A10: (f1 + f2) . x = (f1 . x) + (f2 . x) by A5, A8, VALUED_1:def 1
.= 1 + (f2 . x) by A3, A8
.= 1 + (x #Z (1 + 1)) by A2, TAYLOR_1:def 1
.= 1 + ((x #Z 1) * (x #Z 1)) by TAYLOR_1:1
.= 1 + (x * (x #Z 1)) by PREPOWER:45
.= 1 + (x * x) by PREPOWER:45 ;
(f1 + f2) . x > 0 by A10, XREAL_1:36, XREAL_1:65;
hence ln * (f1 + f2) is_differentiable_in x by A9, TAYLOR_1:20; :: thesis: verum

end;

then A11: ln * (f1 + f2) is_differentiable_on Z by A4, FDIFF_1:16;
for x being Real st x in Z holds
(((1 / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (1 + (x ^2 ))

proof

let x be Real; :: thesis: ( x in Z implies (((1 / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (1 + (x ^2 )) )
assume A12: x in Z ; :: thesis: (((1 / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (1 + (x ^2 ))
A13: f1 + f2 is_differentiable_in x by A6, A12, FDIFF_1:16;
A14: (f1 + f2) . x = (f1 . x) + (f2 . x) by A5, A12, VALUED_1:def 1
.= 1 + (f2 . x) by A3, A12
.= 1 + (x #Z (1 + 1)) by A2, TAYLOR_1:def 1
.= 1 + ((x #Z 1) * (x #Z 1)) by TAYLOR_1:1
.= 1 + (x * (x #Z 1)) by PREPOWER:45
.= 1 + (x * x) by PREPOWER:45 ;
A15: (f1 + f2) . x > 0 by A14, XREAL_1:36, XREAL_1:65;
A16: diff (ln * (f1 + f2)),x = (diff (f1 + f2),x) / ((f1 + f2) . x) by A13, A15, TAYLOR_1:20
.= (((f1 + f2) `| Z) . x) / ((f1 + f2) . x) by A6, A12, FDIFF_1:def 8
.= (2 * x) / (1 + (x ^2 )) by A2, A3, A5, A12, A14, Th99 ;
thus (((1 / 2) (#) (ln * (f1 + f2))) `| Z) . x = (1 / 2) * ((2 * x) / (1 + (x ^2 ))) by A1, A11, A12, A16, FDIFF_1:28
.= x / (1 + (x ^2 )) ; :: thesis: verum

end;

hence ( (1 / 2) (#) (ln * (f1 + f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (1 + (x ^2 )) ) ) by A1, A11, FDIFF_1:28; :: thesis: verum