let Z be open Subset of REAL; :: thesis: for f, f1 being PartFunc of REAL,REAL st Z c= dom f & f = ln * (exp_R / ((#Z 2) * (f1 + exp_R))) & ( for x being Real st x in Z holds
f1 . x = 1 ) holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = (1 - (exp_R . x)) / (1 + (exp_R . x)) ) )
let f, f1 be PartFunc of REAL,REAL; :: thesis: ( Z c= dom f & f = ln * (exp_R / ((#Z 2) * (f1 + exp_R))) & ( for x being Real st x in Z holds
f1 . x = 1 ) implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = (1 - (exp_R . x)) / (1 + (exp_R . x)) ) ) )
assume that
A1: Z c= dom f and
A2: f = ln * (exp_R / ((#Z 2) * (f1 + exp_R))) and
A3: for x being Real st x in Z holds
f1 . x = 1 ; :: thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = (1 - (exp_R . x)) / (1 + (exp_R . x)) ) )
for y being object st y in Z holds
y in dom (exp_R / ((#Z 2) * (f1 + exp_R))) by A1, A2, FUNCT_1:11;
then A4: Z c= dom (exp_R / ((#Z 2) * (f1 + exp_R))) by TARSKI:def 3;
then Z c= (dom exp_R) /\ ((dom ((#Z 2) * (f1 + exp_R))) \ (((#Z 2) * (f1 + exp_R)) " {0})) by RFUNCT_1:def 1;
then A5: Z c= dom ((#Z 2) * (f1 + exp_R)) by XBOOLE_1:1;
then A6: (#Z 2) * (f1 + exp_R) is_differentiable_on Z by A3, Th29;
for y being object st y in Z holds
y in dom (f1 + exp_R) by A5, FUNCT_1:11;
then A7: Z c= dom (f1 + exp_R) by TARSKI:def 3;
A8: for x being Real st x in Z holds
((#Z 2) * (f1 + exp_R)) . x > 0

proof

let x be Real; :: thesis: ( x in Z implies ((#Z 2) * (f1 + exp_R)) . x > 0 )
assume A9: x in Z ; :: thesis: ((#Z 2) * (f1 + exp_R)) . x > 0
then (f1 + exp_R) . x = (f1 . x) + (exp_R . x) by A7, VALUED_1:def 1
.= 1 + (exp_R . x) by A3, A9 ;
then A10: (f1 + exp_R) . x > 0 by SIN_COS:54, XREAL_1:34;
((#Z 2) * (f1 + exp_R)) . x = (#Z 2) . ((f1 + exp_R) . x) by A5, A9, FUNCT_1:12
.= ((f1 + exp_R) . x) #Z 2 by TAYLOR_1:def 1 ;
hence ((#Z 2) * (f1 + exp_R)) . x > 0 by A10, PREPOWER:39; :: thesis: verum

end;

A11: for x being Real st x in Z holds
(exp_R / ((#Z 2) * (f1 + exp_R))) . x > 0

proof

let x be Real; :: thesis: ( x in Z implies (exp_R / ((#Z 2) * (f1 + exp_R))) . x > 0 )
A12: exp_R . x > 0 by SIN_COS:54;
assume A13: x in Z ; :: thesis: (exp_R / ((#Z 2) * (f1 + exp_R))) . x > 0
then A14: ((#Z 2) * (f1 + exp_R)) . x > 0 by A8;
(exp_R / ((#Z 2) * (f1 + exp_R))) . x = (exp_R . x) * ((((#Z 2) * (f1 + exp_R)) . x) ") by A4, A13, RFUNCT_1:def 1
.= (exp_R . x) * (1 / (((#Z 2) * (f1 + exp_R)) . x)) by XCMPLX_1:215
.= (exp_R . x) / (((#Z 2) * (f1 + exp_R)) . x) by XCMPLX_1:99 ;
hence (exp_R / ((#Z 2) * (f1 + exp_R))) . x > 0 by A14, A12, XREAL_1:139; :: thesis: verum

end;

( exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((#Z 2) * (f1 + exp_R)) . x <> 0 ) ) by A8, FDIFF_1:26, TAYLOR_1:16;
then A15: exp_R / ((#Z 2) * (f1 + exp_R)) is_differentiable_on Z by A6, FDIFF_2:21;
A16: for x being Real st x in Z holds
ln * (exp_R / ((#Z 2) * (f1 + exp_R))) is_differentiable_in x

proof

let x be Real; :: thesis: ( x in Z implies ln * (exp_R / ((#Z 2) * (f1 + exp_R))) is_differentiable_in x )
assume x in Z ; :: thesis: ln * (exp_R / ((#Z 2) * (f1 + exp_R))) is_differentiable_in x
then ( exp_R / ((#Z 2) * (f1 + exp_R)) is_differentiable_in x & (exp_R / ((#Z 2) * (f1 + exp_R))) . x > 0 ) by A15, A11, FDIFF_1:9;
hence ln * (exp_R / ((#Z 2) * (f1 + exp_R))) is_differentiable_in x by TAYLOR_1:20; :: thesis: verum

end;

then A17: f is_differentiable_on Z by A1, A2, FDIFF_1:9;
for x being Real st x in Z holds
(f `| Z) . x = (1 - (exp_R . x)) / (1 + (exp_R . x))

proof

let x be Real; :: thesis: ( x in Z implies (f `| Z) . x = (1 - (exp_R . x)) / (1 + (exp_R . x)) )
A18: exp_R is_differentiable_in x by SIN_COS:65;
assume A19: x in Z ; :: thesis: (f `| Z) . x = (1 - (exp_R . x)) / (1 + (exp_R . x))
then A20: ((#Z 2) * (f1 + exp_R)) . x = (#Z 2) . ((f1 + exp_R) . x) by A5, FUNCT_1:12
.= ((f1 + exp_R) . x) #Z 2 by TAYLOR_1:def 1
.= ((f1 . x) + (exp_R . x)) #Z 2 by A7, A19, VALUED_1:def 1
.= (1 + (exp_R . x)) #Z 2 by A3, A19 ;
( ((#Z 2) * (f1 + exp_R)) . x <> 0 & (#Z 2) * (f1 + exp_R) is_differentiable_in x ) by A6, A8, A19, FDIFF_1:9;
then A21: diff ((exp_R / ((#Z 2) * (f1 + exp_R))),x) = (((diff (exp_R,x)) * (((#Z 2) * (f1 + exp_R)) . x)) - ((diff (((#Z 2) * (f1 + exp_R)),x)) * (exp_R . x))) / ((((#Z 2) * (f1 + exp_R)) . x) ^2) by A18, FDIFF_2:14
.= (((exp_R . x) * (((#Z 2) * (f1 + exp_R)) . x)) - ((diff (((#Z 2) * (f1 + exp_R)),x)) * (exp_R . x))) / ((((#Z 2) * (f1 + exp_R)) . x) ^2) by SIN_COS:65
.= (((exp_R . x) * (((#Z 2) * (f1 + exp_R)) . x)) - (((((#Z 2) * (f1 + exp_R)) `| Z) . x) * (exp_R . x))) / ((((#Z 2) * (f1 + exp_R)) . x) ^2) by A6, A19, FDIFF_1:def 7
.= (((exp_R . x) * ((1 + (exp_R . x)) #Z 2)) - (((2 * (exp_R . x)) * (1 + (exp_R . x))) * (exp_R . x))) / (((1 + (exp_R . x)) #Z 2) ^2) by A3, A5, A19, A20, Th29
.= ((exp_R . x) * (((1 + (exp_R . x)) #Z 2) - ((2 * (1 + (exp_R . x))) * (exp_R . x)))) / (((1 + (exp_R . x)) #Z 2) * ((1 + (exp_R . x)) #Z 2))
.= (((exp_R . x) / ((1 + (exp_R . x)) #Z 2)) * (((1 + (exp_R . x)) #Z 2) - ((2 * (1 + (exp_R . x))) * (exp_R . x)))) / ((1 + (exp_R . x)) #Z 2) by XCMPLX_1:83 ;
A22: 1 + (exp_R . x) > 0 by SIN_COS:54, XREAL_1:34;
then ( exp_R . x > 0 & (1 + (exp_R . x)) #Z 2 > 0 ) by PREPOWER:39, SIN_COS:54;
then A23: (exp_R . x) / ((1 + (exp_R . x)) #Z 2) <> 0 by XREAL_1:139;
A24: (exp_R / ((#Z 2) * (f1 + exp_R))) . x = (exp_R . x) * ((((#Z 2) * (f1 + exp_R)) . x) ") by A4, A19, RFUNCT_1:def 1
.= (exp_R . x) * (1 / (((#Z 2) * (f1 + exp_R)) . x)) by XCMPLX_1:215
.= (exp_R . x) / ((1 + (exp_R . x)) #Z 2) by A20, XCMPLX_1:99 ;
A25: ( exp_R / ((#Z 2) * (f1 + exp_R)) is_differentiable_in x & (exp_R / ((#Z 2) * (f1 + exp_R))) . x > 0 ) by A15, A11, A19, FDIFF_1:9;
A26: (1 + (exp_R . x)) #Z 2 = (1 + (exp_R . x)) #Z (1 + 1)
.= ((1 + (exp_R . x)) #Z 1) * ((1 + (exp_R . x)) #Z 1) by A22, PREPOWER:44
.= (1 + (exp_R . x)) * ((1 + (exp_R . x)) #Z 1) by PREPOWER:35
.= (1 + (exp_R . x)) * (1 + (exp_R . x)) by PREPOWER:35 ;
(f `| Z) . x = diff ((ln * (exp_R / ((#Z 2) * (f1 + exp_R)))),x) by A2, A17, A19, FDIFF_1:def 7
.= ((((exp_R . x) / ((1 + (exp_R . x)) #Z 2)) * (((1 + (exp_R . x)) #Z 2) - ((2 * (1 + (exp_R . x))) * (exp_R . x)))) / ((1 + (exp_R . x)) #Z 2)) / ((exp_R . x) / ((1 + (exp_R . x)) #Z 2)) by A25, A21, A24, TAYLOR_1:20
.= (((exp_R . x) / ((1 + (exp_R . x)) #Z 2)) * (((1 + (exp_R . x)) #Z 2) - ((2 * (1 + (exp_R . x))) * (exp_R . x)))) / (((exp_R . x) / ((1 + (exp_R . x)) #Z 2)) * ((1 + (exp_R . x)) #Z 2)) by XCMPLX_1:78
.= ((1 + (exp_R . x)) * (1 - (exp_R . x))) / ((1 + (exp_R . x)) * (1 + (exp_R . x))) by A23, A26, XCMPLX_1:91
.= (1 - (exp_R . x)) / (1 + (exp_R . x)) by A22, XCMPLX_1:91 ;
hence (f `| Z) . x = (1 - (exp_R . x)) / (1 + (exp_R . x)) ; :: thesis: verum

end;

hence ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = (1 - (exp_R . x)) / (1 + (exp_R . x)) ) ) by A1, A2, A16, FDIFF_1:9; :: thesis: verum