let r be Real; :: thesis: for Z being open Subset of REAL
for f1, f2, f being PartFunc of REAL ,REAL st Z c= dom ((r / 2) (#) (ln * (f1 + f2))) & ( for x being Real st x in Z holds
f1 . x = 1 ) & r <> 0 & f2 = (#Z 2) * f & ( for x being Real st x in Z holds
f . x = x / r ) holds
( (r / 2) (#) (ln * (f1 + f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((r / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (r * (1 + ((x / r) ^2 ))) ) )
let Z be open Subset of REAL ; :: thesis: for f1, f2, f being PartFunc of REAL ,REAL st Z c= dom ((r / 2) (#) (ln * (f1 + f2))) & ( for x being Real st x in Z holds
f1 . x = 1 ) & r <> 0 & f2 = (#Z 2) * f & ( for x being Real st x in Z holds
f . x = x / r ) holds
( (r / 2) (#) (ln * (f1 + f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((r / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (r * (1 + ((x / r) ^2 ))) ) )
let f1, f2, f be PartFunc of REAL ,REAL ; :: thesis: ( Z c= dom ((r / 2) (#) (ln * (f1 + f2))) & ( for x being Real st x in Z holds
f1 . x = 1 ) & r <> 0 & f2 = (#Z 2) * f & ( for x being Real st x in Z holds
f . x = x / r ) implies ( (r / 2) (#) (ln * (f1 + f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((r / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (r * (1 + ((x / r) ^2 ))) ) ) )
assume that
A1: Z c= dom ((r / 2) (#) (ln * (f1 + f2))) and
A2: for x being Real st x in Z holds
f1 . x = 1 and
A3: r <> 0 and
A4: ( f2 = (#Z 2) * f & ( for x being Real st x in Z holds
f . x = x / r ) ) ; :: thesis: ( (r / 2) (#) (ln * (f1 + f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((r / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (r * (1 + ((x / r) ^2 ))) ) )
A5: 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 A6: Z c= dom (f1 + f2) by TARSKI:def 3;
dom (f1 + f2) = (dom f1) /\ (dom f2) by VALUED_1:def 1;
then A7: ( Z c= dom f1 & Z c= dom f2 ) by A6, XBOOLE_1:18;
A8: ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + f2) `| Z) . x = (2 * x) / (r ^2 ) ) ) by A2, A4, A6, Th105;
for x being Real st x in Z holds
ln * (f1 + f2) is_differentiable_in x

proof

set g = #Z 2;
let x be Real; :: thesis: ( x in Z implies ln * (f1 + f2) is_differentiable_in x )
assume A10: x in Z ; :: thesis: ln * (f1 + f2) is_differentiable_in x
then A11: f1 + f2 is_differentiable_in x by A8, FDIFF_1:16;
A13: (f1 + f2) . x = (f1 . x) + (f2 . x) by A6, A10, VALUED_1:def 1
.= 1 + (((#Z 2) * f) . x) by A2, A4, A10
.= 1 + ((#Z 2) . (f . x)) by A4, A7, A10, FUNCT_1:22
.= 1 + ((#Z 2) . (x / r)) by A4, A10
.= 1 + ((x / r) #Z (1 + 1)) by TAYLOR_1:def 1
.= 1 + (((x / r) #Z 1) * ((x / r) #Z 1)) by TAYLOR_1:1
.= 1 + ((x / r) * ((x / r) #Z 1)) by PREPOWER:45
.= 1 + ((x / r) * (x / r)) by PREPOWER:45 ;
(f1 + f2) . x > 0 by A13, XREAL_1:36, XREAL_1:65;
hence ln * (f1 + f2) is_differentiable_in x by A11, TAYLOR_1:20; :: thesis: verum

end;

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

proof

set g = #Z 2;
let x be Real; :: thesis: ( x in Z implies (((r / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (r * (1 + ((x / r) ^2 ))) )
assume A15: x in Z ; :: thesis: (((r / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (r * (1 + ((x / r) ^2 )))
A16: f1 + f2 is_differentiable_in x by A8, A15, FDIFF_1:16;
A17: (f1 + f2) . x = (f1 . x) + (f2 . x) by A6, A15, VALUED_1:def 1
.= 1 + (((#Z 2) * f) . x) by A2, A4, A15
.= 1 + ((#Z 2) . (f . x)) by A4, A7, A15, FUNCT_1:22
.= 1 + ((#Z 2) . (x / r)) by A4, A15
.= 1 + ((x / r) #Z (1 + 1)) by TAYLOR_1:def 1
.= 1 + (((x / r) #Z 1) * ((x / r) #Z 1)) by TAYLOR_1:1
.= 1 + ((x / r) * ((x / r) #Z 1)) by PREPOWER:45
.= 1 + ((x / r) * (x / r)) by PREPOWER:45 ;
A18: (f1 + f2) . x > 0 by A17, XREAL_1:36, XREAL_1:65;
A19: diff (ln * (f1 + f2)),x = (diff (f1 + f2),x) / ((f1 + f2) . x) by A16, A18, TAYLOR_1:20
.= (((f1 + f2) `| Z) . x) / ((f1 + f2) . x) by A8, A15, FDIFF_1:def 8
.= ((2 * x) / (r ^2 )) / (1 + ((x / r) ^2 )) by A2, A4, A6, A15, A17, Th105 ;
thus (((r / 2) (#) (ln * (f1 + f2))) `| Z) . x = (r / 2) * (diff (ln * (f1 + f2)),x) by A1, A14, A15, FDIFF_1:28
.= ((r * x) / (r ^2 )) / (1 + ((x / r) ^2 )) by A19
.= ((r / r) * (x / r)) / (1 + ((x / r) ^2 )) by XCMPLX_1:77
.= (1 * (x / r)) / (1 + ((x / r) ^2 )) by A3, XCMPLX_1:60
.= x / (r * (1 + ((x / r) ^2 ))) by XCMPLX_1:79 ; :: thesis: verum

end;

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