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 & f = ln * (exp_R / ((#Z 2) * (f1 + exp_R ))) ) and
A2: 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 set st y in Z holds
y in dom (exp_R / ((#Z 2) * (f1 + exp_R ))) by A1, FUNCT_1:21;
then A3: 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 4;
then A4: Z c= dom ((#Z 2) * (f1 + exp_R )) by XBOOLE_1:1;
then A5: ( (#Z 2) * (f1 + exp_R ) is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z 2) * (f1 + exp_R )) `| Z) . x = (2 * (exp_R . x)) * (1 + (exp_R . x)) ) ) by A2, Th29;
A6: exp_R is_differentiable_on Z by FDIFF_1:34, TAYLOR_1:16;
for y being set st y in Z holds
y in dom (f1 + exp_R ) by A4, FUNCT_1:21;
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 A10: ((#Z 2) * (f1 + exp_R )) . x = (#Z 2) . ((f1 + exp_R ) . x) by A4, FUNCT_1:22
.= ((f1 + exp_R ) . x) #Z 2 by TAYLOR_1:def 1 ;
(f1 + exp_R ) . x = (f1 . x) + (exp_R . x) by A7, A9, VALUED_1:def 1
.= 1 + (exp_R . x) by A2, A9 ;
then (f1 + exp_R ) . x > 0 by SIN_COS:59, XREAL_1:36;
hence ((#Z 2) * (f1 + exp_R )) . x > 0 by A10, PREPOWER:49; :: thesis: verum

end;

then for x being Real st x in Z holds
((#Z 2) * (f1 + exp_R )) . x <> 0 ;
then A11: exp_R / ((#Z 2) * (f1 + exp_R )) is_differentiable_on Z by A5, A6, FDIFF_2:21;
A12: 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 )
assume A13: x in Z ; :: thesis: (exp_R / ((#Z 2) * (f1 + exp_R ))) . x > 0
then A14: (exp_R / ((#Z 2) * (f1 + exp_R ))) . x = (exp_R . x) * ((((#Z 2) * (f1 + exp_R )) . x) " ) by A3, RFUNCT_1:def 4
.= (exp_R . x) * (1 / (((#Z 2) * (f1 + exp_R )) . x)) by XCMPLX_1:217
.= (exp_R . x) / (((#Z 2) * (f1 + exp_R )) . x) by XCMPLX_1:100 ;
A15: ((#Z 2) * (f1 + exp_R )) . x > 0 by A8, A13;
exp_R . x > 0 by SIN_COS:59;
hence (exp_R / ((#Z 2) * (f1 + exp_R ))) . x > 0 by A14, A15, XREAL_1:141; :: thesis: verum

end;

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 A17: x in Z ; :: thesis: ln * (exp_R / ((#Z 2) * (f1 + exp_R ))) is_differentiable_in x
then A18: exp_R / ((#Z 2) * (f1 + exp_R )) is_differentiable_in x by A11, FDIFF_1:16;
(exp_R / ((#Z 2) * (f1 + exp_R ))) . x > 0 by A12, A17;
hence ln * (exp_R / ((#Z 2) * (f1 + exp_R ))) is_differentiable_in x by A18, TAYLOR_1:20; :: thesis: verum

end;

then A19: f is_differentiable_on Z by A1, FDIFF_1:16;
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)) )
assume A20: x in Z ; :: thesis: (f `| Z) . x = (1 - (exp_R . x)) / (1 + (exp_R . x))
then A21: ((#Z 2) * (f1 + exp_R )) . x <> 0 by A8;
A22: (#Z 2) * (f1 + exp_R ) is_differentiable_in x by A5, A20, FDIFF_1:16;
A23: exp_R is_differentiable_in x by SIN_COS:70;
A24: exp_R / ((#Z 2) * (f1 + exp_R )) is_differentiable_in x by A11, A20, FDIFF_1:16;
A25: (exp_R / ((#Z 2) * (f1 + exp_R ))) . x > 0 by A12, A20;
A26: exp_R . x > 0 by SIN_COS:59;
A27: 1 + (exp_R . x) > 0 by SIN_COS:59, XREAL_1:36;
then (1 + (exp_R . x)) #Z 2 > 0 by PREPOWER:49;
then A28: (exp_R . x) / ((1 + (exp_R . x)) #Z 2) <> 0 by A26, XREAL_1:141;
A29: ((#Z 2) * (f1 + exp_R )) . x = (#Z 2) . ((f1 + exp_R ) . x) by A4, A20, FUNCT_1:22
.= ((f1 + exp_R ) . x) #Z 2 by TAYLOR_1:def 1
.= ((f1 . x) + (exp_R . x)) #Z 2 by A7, A20, VALUED_1:def 1
.= (1 + (exp_R . x)) #Z 2 by A2, A20 ;
A30: 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 A21, A22, A23, 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:70
.= (((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 A5, A20, FDIFF_1:def 8
.= (((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 A2, A4, A20, A29, 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:84 ;
A31: (exp_R / ((#Z 2) * (f1 + exp_R ))) . x = (exp_R . x) * ((((#Z 2) * (f1 + exp_R )) . x) " ) by A3, A20, RFUNCT_1:def 4
.= (exp_R . x) * (1 / (((#Z 2) * (f1 + exp_R )) . x)) by XCMPLX_1:217
.= (exp_R . x) / ((1 + (exp_R . x)) #Z 2) by A29, XCMPLX_1:100 ;
A32: (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 A27, PREPOWER:54
.= (1 + (exp_R . x)) * ((1 + (exp_R . x)) #Z 1) by PREPOWER:45
.= (1 + (exp_R . x)) * (1 + (exp_R . x)) by PREPOWER:45 ;
(f `| Z) . x = diff (ln * (exp_R / ((#Z 2) * (f1 + exp_R )))),x by A1, A19, A20, FDIFF_1:def 8
.= ((((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 A24, A25, A30, A31, 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:79
.= ((1 + (exp_R . x)) * (1 - (exp_R . x))) / ((1 + (exp_R . x)) * (1 + (exp_R . x))) by A28, A32, XCMPLX_1:92
.= (1 - (exp_R . x)) / (1 + (exp_R . x)) by A27, XCMPLX_1:92 ;
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, A16, FDIFF_1:16; :: thesis: verum