let Z be open Subset of REAL; :: thesis: for g being PartFunc of REAL,REAL st Z c= dom (g (#) ln) & g = #Z 2 & ( for x being Real st x in Z holds
x > 0 ) holds
( g (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) ) )
let g be PartFunc of REAL,REAL; :: thesis: ( Z c= dom (g (#) ln) & g = #Z 2 & ( for x being Real st x in Z holds
x > 0 ) implies ( g (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) ) ) )
set f = ln ;
assume that
A1: Z c= dom (g (#) ln) and
A2: g = #Z 2 and
A3: for x being Real st x in Z holds
x > 0 ; :: thesis: ( g (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) ) )
A4: for x being Real st x in Z holds
g is_differentiable_in x by A2, TAYLOR_1:2;
A5: Z c= (dom g) /\ (dom ln) by A1, VALUED_1:def 4;
then A6: Z c= dom ln by XBOOLE_1:18;
then A7: ln is_differentiable_on Z by Th19;
Z c= dom g by A5, XBOOLE_1:18;
then A8: g is_differentiable_on Z by A4, FDIFF_1:9;
A9: for x being Real st x in Z holds
(g `| Z) . x = 2 * x

proof

let x be Real; :: thesis: ( x in Z implies (g `| Z) . x = 2 * x )
assume A10: x in Z ; :: thesis: (g `| Z) . x = 2 * x
diff (g,x) = 2 * (x #Z (2 - 1)) by A2, TAYLOR_1:2
.= 2 * x by PREPOWER:35 ;
hence (g `| Z) . x = 2 * x by A8, A10, FDIFF_1:def 7; :: thesis: verum

end;

now :: thesis: for x being Real st x in Z holds
((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x))

let x be Real; :: thesis: ( x in Z implies ((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) )
assume A11: x in Z ; :: thesis: ((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x))
then A12: x <> 0 by A3;
((g (#) ln) `| Z) . x = ((g . x) * (diff (ln,x))) + ((ln . x) * (diff (g,x))) by A1, A8, A7, A11, FDIFF_1:21
.= ((g . x) * ((ln `| Z) . x)) + ((ln . x) * (diff (g,x))) by A7, A11, FDIFF_1:def 7
.= ((g . x) * (1 / x)) + ((ln . x) * (diff (g,x))) by A6, A11, Th19
.= ((x #Z 2) * (1 / x)) + ((ln . x) * (diff (g,x))) by A2, TAYLOR_1:def 1
.= ((x #Z 2) * (1 / x)) + ((ln . x) * ((g `| Z) . x)) by A8, A11, FDIFF_1:def 7
.= ((x #Z (1 + 1)) * (1 / x)) + ((2 * x) * (ln . x)) by A9, A11
.= (((x #Z 1) * (x #Z 1)) * (1 / x)) + ((2 * x) * (ln . x)) by TAYLOR_1:1
.= (((x #Z 1) * x) * (1 / x)) + ((2 * x) * (ln . x)) by PREPOWER:35
.= ((x * x) * (1 / x)) + ((2 * x) * (ln . x)) by PREPOWER:35
.= (x * (x * (1 / x))) + ((2 * x) * (ln . x))
.= (x * 1) + ((2 * x) * (ln . x)) by A12, XCMPLX_1:106
.= x + ((2 * x) * (ln . x)) ;
hence ((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) ; :: thesis: verum

end;

hence ( g (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) ) ) by A1, A8, A7, FDIFF_1:21; :: thesis: verum