let Z be open Subset of REAL ; :: thesis: for f, f1 being PartFunc of REAL ,REAL st Z c= dom f & f = ln * (((#Z 2) * (exp_R + 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 = ((exp_R . x) - 1) / ((exp_R . x) + 1) ) )
let f, f1 be PartFunc of REAL ,REAL ; :: thesis: ( Z c= dom f & f = ln * (((#Z 2) * (exp_R + 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 = ((exp_R . x) - 1) / ((exp_R . x) + 1) ) ) )
assume that
A1: ( Z c= dom f & f = ln * (((#Z 2) * (exp_R + 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 = ((exp_R . x) - 1) / ((exp_R . x) + 1) ) )
for y being set st y in Z holds
y in dom (((#Z 2) * (exp_R + f1)) / exp_R ) by A1, FUNCT_1:21;
then A3: Z c= dom (((#Z 2) * (exp_R + f1)) / exp_R ) by TARSKI:def 3;
then Z c= (dom ((#Z 2) * (exp_R + f1))) /\ ((dom exp_R ) \ (exp_R " {0 })) by RFUNCT_1:def 4;
then A4: Z c= dom ((#Z 2) * (exp_R + f1)) by XBOOLE_1:18;
then A5: ( (#Z 2) * (exp_R + f1) is_differentiable_on Z & ( for x being Real st x in Z holds
(((#Z 2) * (exp_R + f1)) `| Z) . x = (2 * (exp_R . x)) * ((exp_R . x) + 1) ) ) by A2, Th29;
A6: exp_R is_differentiable_on Z by FDIFF_1:34, TAYLOR_1:16;
for x being Real st x in Z holds
exp_R . x <> 0 by SIN_COS:59;
then A7: ((#Z 2) * (exp_R + f1)) / exp_R is_differentiable_on Z by A5, A6, FDIFF_2:21;
for y being set st y in Z holds
y in dom (exp_R + f1) by A4, FUNCT_1:21;
then A8: Z c= dom (exp_R + f1) by TARSKI:def 3;
A9: for x being Real st x in Z holds
(((#Z 2) * (exp_R + f1)) / exp_R ) . x > 0

proof

let x be Real; :: thesis: ( x in Z implies (((#Z 2) * (exp_R + f1)) / exp_R ) . x > 0 )
assume A10: x in Z ; :: thesis: (((#Z 2) * (exp_R + f1)) / exp_R ) . x > 0
then A11: (((#Z 2) * (exp_R + f1)) / exp_R ) . x = (((#Z 2) * (exp_R + f1)) . x) * ((exp_R . x) " ) by A3, RFUNCT_1:def 4
.= (((#Z 2) * (exp_R + f1)) . x) * (1 / (exp_R . x)) by XCMPLX_1:217
.= (((#Z 2) * (exp_R + f1)) . x) / (exp_R . x) by XCMPLX_1:100
.= ((#Z 2) . ((exp_R + f1) . x)) / (exp_R . x) by A4, A10, FUNCT_1:22
.= (((exp_R + f1) . x) #Z 2) / (exp_R . x) by TAYLOR_1:def 1 ;
(exp_R + f1) . x = (exp_R . x) + (f1 . x) by A8, A10, VALUED_1:def 1
.= (exp_R . x) + 1 by A2, A10 ;
then (exp_R + f1) . x > 0 by SIN_COS:59, XREAL_1:36;
then A12: ((exp_R + f1) . x) #Z 2 > 0 by PREPOWER:49;
exp_R . x > 0 by SIN_COS:59;
hence (((#Z 2) * (exp_R + f1)) / exp_R ) . x > 0 by A11, A12, XREAL_1:141; :: thesis: verum

end;

A13: for x being Real st x in Z holds
ln * (((#Z 2) * (exp_R + f1)) / exp_R ) is_differentiable_in x

proof

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

end;

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

proof

let x be Real; :: thesis: ( x in Z implies (f `| Z) . x = ((exp_R . x) - 1) / ((exp_R . x) + 1) )
assume A17: x in Z ; :: thesis: (f `| Z) . x = ((exp_R . x) - 1) / ((exp_R . x) + 1)
then A18: ((#Z 2) * (exp_R + f1)) / exp_R is_differentiable_in x by A7, FDIFF_1:16;
A19: (((#Z 2) * (exp_R + f1)) / exp_R ) . x > 0 by A9, A17;
A20: exp_R . x > 0 by SIN_COS:59;
A21: (exp_R . x) + 1 > 0 by SIN_COS:59, XREAL_1:36;
A22: (exp_R + f1) . x = (exp_R . x) + (f1 . x) by A8, A17, VALUED_1:def 1
.= (exp_R . x) + 1 by A2, A17 ;
A23: ((#Z 2) * (exp_R + f1)) . x = (#Z 2) . ((exp_R + f1) . x) by A4, A17, FUNCT_1:22
.= ((exp_R . x) + 1) #Z (1 + 1) by A22, TAYLOR_1:def 1
.= (((exp_R . x) + 1) #Z 1) * (((exp_R . x) + 1) #Z 1) by A21, PREPOWER:54
.= ((exp_R . x) + 1) * (((exp_R . x) + 1) #Z 1) by PREPOWER:45
.= ((exp_R . x) + 1) * ((exp_R . x) + 1) by PREPOWER:45 ;
A24: (#Z 2) * (exp_R + f1) is_differentiable_in x by A5, A17, FDIFF_1:16;
exp_R is_differentiable_in x by SIN_COS:70;
then A25: diff (((#Z 2) * (exp_R + f1)) / exp_R ),x = (((diff ((#Z 2) * (exp_R + f1)),x) * (exp_R . x)) - ((diff exp_R ,x) * (((#Z 2) * (exp_R + f1)) . x))) / ((exp_R . x) ^2 ) by A20, A24, FDIFF_2:14
.= ((((((#Z 2) * (exp_R + f1)) `| Z) . x) * (exp_R . x)) - ((diff exp_R ,x) * (((#Z 2) * (exp_R + f1)) . x))) / ((exp_R . x) ^2 ) by A5, A17, FDIFF_1:def 8
.= ((((2 * (exp_R . x)) * ((exp_R . x) + 1)) * (exp_R . x)) - ((diff exp_R ,x) * (((#Z 2) * (exp_R + f1)) . x))) / ((exp_R . x) ^2 ) by A2, A4, A17, Th29
.= ((((2 * (exp_R . x)) * ((exp_R . x) + 1)) * (exp_R . x)) - ((exp_R . x) * (((#Z 2) * (exp_R + f1)) . x))) / ((exp_R . x) ^2 ) by SIN_COS:70
.= ((((2 * (exp_R . x)) * ((exp_R . x) + 1)) - (((#Z 2) * (exp_R + f1)) . x)) * (exp_R . x)) / ((exp_R . x) * (exp_R . x))
.= (((exp_R . x) - 1) * ((exp_R . x) + 1)) / (exp_R . x) by A20, A23, XCMPLX_1:92 ;
A26: (((#Z 2) * (exp_R + f1)) / exp_R ) . x = (((#Z 2) * (exp_R + f1)) . x) * ((exp_R . x) " ) by A3, A17, RFUNCT_1:def 4
.= (((#Z 2) * (exp_R + f1)) . x) * (1 / (exp_R . x)) by XCMPLX_1:217
.= (((exp_R . x) + 1) * ((exp_R . x) + 1)) / (exp_R . x) by A23, XCMPLX_1:100 ;
(f `| Z) . x = diff (ln * (((#Z 2) * (exp_R + f1)) / exp_R )),x by A1, A16, A17, FDIFF_1:def 8
.= ((((exp_R . x) + 1) * ((exp_R . x) - 1)) / (exp_R . x)) / ((((exp_R . x) + 1) * ((exp_R . x) + 1)) / (exp_R . x)) by A18, A19, A25, A26, TAYLOR_1:20
.= (((exp_R . x) + 1) * ((exp_R . x) - 1)) / (((exp_R . x) + 1) * ((exp_R . x) + 1)) by A20, XCMPLX_1:55
.= ((exp_R . x) - 1) / ((exp_R . x) + 1) by A21, XCMPLX_1:92 ;
hence (f `| Z) . x = ((exp_R . x) - 1) / ((exp_R . x) + 1) ; :: thesis: verum

end;

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