let Z be open Subset of REAL; :: thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom ((f2 ^) + (ln * (f1 / f2))) & ( for x being Real st x in Z holds
( f2 . x = x & f2 . x > 0 & f1 . x = x - 1 & f1 . x > 0 ) ) holds
( (f2 ^) + (ln * (f1 / f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((f2 ^) + (ln * (f1 / f2))) `| Z) . x = 1 / ((x ^2) * (x - 1)) ) )
let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( Z c= dom ((f2 ^) + (ln * (f1 / f2))) & ( for x being Real st x in Z holds
( f2 . x = x & f2 . x > 0 & f1 . x = x - 1 & f1 . x > 0 ) ) implies ( (f2 ^) + (ln * (f1 / f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((f2 ^) + (ln * (f1 / f2))) `| Z) . x = 1 / ((x ^2) * (x - 1)) ) ) )
assume that
A1: Z c= dom ((f2 ^) + (ln * (f1 / f2))) and
A2: for x being Real st x in Z holds
( f2 . x = x & f2 . x > 0 & f1 . x = x - 1 & f1 . x > 0 ) ; :: thesis: ( (f2 ^) + (ln * (f1 / f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((f2 ^) + (ln * (f1 / f2))) `| Z) . x = 1 / ((x ^2) * (x - 1)) ) )
A3: Z c= (dom (f2 ^)) /\ (dom (ln * (f1 / f2))) by A1, VALUED_1:def 1;
then A4: Z c= dom (ln * (f1 / f2)) by XBOOLE_1:18;
A5: dom (f2 ^) c= dom f2 by RFUNCT_1:1;
Z c= dom (f2 ^) by A3, XBOOLE_1:18;
then A6: Z c= dom f2 by A5, XBOOLE_1:1;
A7: for x being Real st x in Z holds
( f1 . x = x - 1 & f1 . x > 0 & f2 . x = x - 0 & f2 . x > 0 ) by A2;
then A8: ln * (f1 / f2) is_differentiable_on Z by A4, FDIFF_4:24;
A9: for x being Real st x in Z holds
( f2 . x = 0 + x & f2 . x <> 0 ) by A2;
then A10: f2 ^ is_differentiable_on Z by A6, FDIFF_4:14;
for x being Real st x in Z holds
(((f2 ^) + (ln * (f1 / f2))) `| Z) . x = 1 / ((x ^2) * (x - 1))

proof

let x be Real; :: thesis: ( x in Z implies (((f2 ^) + (ln * (f1 / f2))) `| Z) . x = 1 / ((x ^2) * (x - 1)) )
assume A11: x in Z ; :: thesis: (((f2 ^) + (ln * (f1 / f2))) `| Z) . x = 1 / ((x ^2) * (x - 1))
then A12: ( f2 . x = x & f2 . x > 0 ) by A2;
A13: ( f1 . x = x - 1 & f1 . x > 0 ) by A2, A11;
(((f2 ^) + (ln * (f1 / f2))) `| Z) . x = (diff ((f2 ^),x)) + (diff ((ln * (f1 / f2)),x)) by A1, A10, A8, A11, FDIFF_1:18
.= (((f2 ^) `| Z) . x) + (diff ((ln * (f1 / f2)),x)) by A10, A11, FDIFF_1:def 7
.= (((f2 ^) `| Z) . x) + (((ln * (f1 / f2)) `| Z) . x) by A8, A11, FDIFF_1:def 7
.= (- (1 / ((0 + x) ^2))) + (((ln * (f1 / f2)) `| Z) . x) by A6, A9, A11, FDIFF_4:14
.= (- (1 / ((0 + x) ^2))) + ((1 - 0) / ((x - 1) * (x - 0))) by A4, A7, A11, FDIFF_4:24
.= (- ((1 * (x - 1)) / ((x ^2) * (x - 1)))) + (1 / ((x - 1) * x)) by A13, XCMPLX_1:91
.= (- ((1 * (x - 1)) / ((x ^2) * (x - 1)))) + ((1 * x) / (((x - 1) * x) * x)) by A12, XCMPLX_1:91
.= ((- (x - 1)) / ((x ^2) * (x - 1))) + (x / ((x ^2) * (x - 1))) by XCMPLX_1:187
.= (((- x) + 1) + x) / ((x ^2) * (x - 1)) by XCMPLX_1:62
.= 1 / ((x ^2) * (x - 1)) ;
hence (((f2 ^) + (ln * (f1 / f2))) `| Z) . x = 1 / ((x ^2) * (x - 1)) ; :: thesis: verum

end;

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