let Z be open Subset of REAL ; :: thesis: for f2, f1 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 f2, f1 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:11;
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:26
.= (((f2 ^ ) `| Z) . x) + (diff (ln * (f1 / f2)),x) by A10, A11, FDIFF_1:def 8
.= (((f2 ^ ) `| Z) . x) + (((ln * (f1 / f2)) `| Z) . x) by A8, A11, FDIFF_1:def 8
.= (- (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:92
.= (- ((1 * (x - 1)) / ((x ^2 ) * (x - 1)))) + ((1 * x) / (((x - 1) * x) * x)) by A12, XCMPLX_1:92
.= ((- (x - 1)) / ((x ^2 ) * (x - 1))) + (x / ((x ^2 ) * (x - 1))) by XCMPLX_1:188
.= (((- x) + 1) + x) / ((x ^2 ) * (x - 1)) by XCMPLX_1:63
.= 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:26; :: thesis: verum