let a be Real; :: thesis: for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 + f2)) & f2 = #Z 3 & ( for x being Real st x in Z holds
( f1 . x = a & (f1 + f2) . x > 0 ) ) holds
( ln * (f1 + f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * (f1 + f2)) `| Z) . x = (3 * (x |^ 2)) / (a + (x |^ 3)) ) )
let Z be open Subset of REAL; :: thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 + f2)) & f2 = #Z 3 & ( for x being Real st x in Z holds
( f1 . x = a & (f1 + f2) . x > 0 ) ) holds
( ln * (f1 + f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * (f1 + f2)) `| Z) . x = (3 * (x |^ 2)) / (a + (x |^ 3)) ) )
let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( Z c= dom (ln * (f1 + f2)) & f2 = #Z 3 & ( for x being Real st x in Z holds
( f1 . x = a & (f1 + f2) . x > 0 ) ) implies ( ln * (f1 + f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * (f1 + f2)) `| Z) . x = (3 * (x |^ 2)) / (a + (x |^ 3)) ) ) )
assume that
A1: Z c= dom (ln * (f1 + f2)) and
A2: f2 = #Z 3 and
A3: for x being Real st x in Z holds
( f1 . x = a & (f1 + f2) . x > 0 ) ; :: thesis: ( ln * (f1 + f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * (f1 + f2)) `| Z) . x = (3 * (x |^ 2)) / (a + (x |^ 3)) ) )
for y being object st y in Z holds
y in dom (f1 + f2) by A1, FUNCT_1:11;
then A4: Z c= dom (f1 + f2) by TARSKI:def 3;
A5: for x being Real st x in Z holds
f1 . x = a by A3;
then A6: f1 + f2 is_differentiable_on Z by A2, A4, Th20;
A7: for x being Real st x in Z holds
ln * (f1 + f2) is_differentiable_in x

proof

let x be Real; :: thesis: ( x in Z implies ln * (f1 + f2) is_differentiable_in x )
assume x in Z ; :: thesis: ln * (f1 + f2) is_differentiable_in x
then ( f1 + f2 is_differentiable_in x & (f1 + f2) . x > 0 ) by A3, A6, FDIFF_1:9;
hence ln * (f1 + f2) is_differentiable_in x by TAYLOR_1:20; :: thesis: verum

end;

then A8: ln * (f1 + f2) is_differentiable_on Z by A1, FDIFF_1:9;
for x being Real st x in Z holds
((ln * (f1 + f2)) `| Z) . x = (3 * (x |^ 2)) / (a + (x |^ 3))

proof

let x be Real; :: thesis: ( x in Z implies ((ln * (f1 + f2)) `| Z) . x = (3 * (x |^ 2)) / (a + (x |^ 3)) )
assume A9: x in Z ; :: thesis: ((ln * (f1 + f2)) `| Z) . x = (3 * (x |^ 2)) / (a + (x |^ 3))
then A10: x in dom (f1 + f2) by A1, FUNCT_1:11;
( f1 + f2 is_differentiable_in x & (f1 + f2) . x > 0 ) by A3, A6, A9, FDIFF_1:9;
then diff ((ln * (f1 + f2)),x) = (diff ((f1 + f2),x)) / ((f1 + f2) . x) by TAYLOR_1:20
.= (((f1 + f2) `| Z) . x) / ((f1 + f2) . x) by A6, A9, FDIFF_1:def 7
.= (3 * (x |^ 2)) / ((f1 + f2) . x) by A2, A4, A5, A9, Th20
.= (3 * (x |^ 2)) / ((f1 . x) + (f2 . x)) by A10, VALUED_1:def 1
.= (3 * (x |^ 2)) / (a + (f2 . x)) by A3, A9
.= (3 * (x |^ 2)) / (a + (x #Z 3)) by A2, TAYLOR_1:def 1
.= (3 * (x |^ 2)) / (a + (x |^ 3)) by PREPOWER:36 ;
hence ((ln * (f1 + f2)) `| Z) . x = (3 * (x |^ 2)) / (a + (x |^ 3)) by A8, A9, FDIFF_1:def 7; :: thesis: verum

end;

hence ( ln * (f1 + f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * (f1 + f2)) `| Z) . x = (3 * (x |^ 2)) / (a + (x |^ 3)) ) ) by A1, A7, FDIFF_1:9; :: thesis: verum