FDIFF_12: Differentiation on Interval

:: Differentiation on Interval
:: by Noboru Endou
::
:: Received March 31, 2023
:: Copyright (c) 2023-2025 Association of Mizar Users

theorem Th1: :: FDIFF_12:1

for A, B being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on A & rng (f1 | A) c= B & f2 is_differentiable_on B holds
( f2 * f1 is_differentiable_on A & (f2 * f1) `| A = ((f2 `| B) * f1) (#) (f1 `| A) )

proof end;

theorem Th2: :: FDIFF_12:2

for I being Interval holds
( ].(inf I),(sup I).[ is open Subset of REAL & ].(inf I),(sup I).[ c= I )

proof end;

theorem Th3: :: FDIFF_12:3

for I being Interval
for x being Real st x in I & x <> inf I & x <> sup I holds
x in ].(inf I),(sup I).[

proof end;

Lm1: for r being set
for I being interval Subset of REAL st r in I & I is closed_interval & not ( r = inf I & r = lower_bound I ) & not ( r = sup I & r = upper_bound I ) holds
r in ].(inf I),(sup I).[

proof end;

Lm2: for r being set
for I being interval Subset of REAL st r in I & I is right_open_interval & not ( r = inf I & r = lower_bound I ) holds
r in ].(inf I),(sup I).[

proof end;

Lm3: for r being set
for I being interval Subset of REAL st r in I & I is left_open_interval & not ( r = sup I & r = upper_bound I ) holds
r in ].(inf I),(sup I).[

proof end;

Lm4: for r being set
for I being interval Subset of REAL st r in I & I is open_interval holds
r in ].(inf I),(sup I).[

proof end;

theorem Th4: :: FDIFF_12:4

for f being PartFunc of REAL,REAL
for I being Interval
for x being Real st f is_right_differentiable_in x & x in I & x <> sup I holds
f | I is_right_differentiable_in x

proof end;

theorem Th5: :: FDIFF_12:5

for f being PartFunc of REAL,REAL
for I being Interval
for x being Real st f is_left_differentiable_in x & x in I & x <> inf I holds
f | I is_left_differentiable_in x

proof end;

theorem Th6: :: FDIFF_12:6

for X being set
for f1, f2 being PartFunc of X,REAL st dom f1 = dom f2 holds
( (f1 + f2) - f2 = f1 & (f1 - f2) + f2 = f1 )

proof end;

definition

let f be PartFunc of REAL,REAL;
let I be non empty Interval;

pred f is_differentiable_on_interval I means :: FDIFF_12:def 1
( I c= dom f & inf I < sup I & ( inf I in I implies f is_right_differentiable_in lower_bound I ) & ( sup I in I implies f is_left_differentiable_in upper_bound I ) & f is_differentiable_on ].(inf I),(sup I).[ );

end;

:: deftheorem defines is_differentiable_on_interval FDIFF_12:def 1 :

Lm5: for I being interval Subset of REAL st inf I in I holds
inf I = lower_bound I

proof end;

Lm6: for I being interval Subset of REAL st sup I in I holds
sup I = upper_bound I

proof end;

definition

let f be PartFunc of REAL,REAL;
let I be non empty interval Subset of REAL;
assume A1: f is_differentiable_on_interval I ;

func f `\ I -> PartFunc of REAL,REAL means :Def2: :: FDIFF_12:def 2
( dom it = I & ( for x being Real st x in I holds
( ( x = inf I implies it . x = Rdiff (f,x) ) & ( x = sup I implies it . x = Ldiff (f,x) ) & ( x <> inf I & x <> sup I implies it . x = diff (f,x) ) ) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines `\ FDIFF_12:def 2 :

theorem :: FDIFF_12:7

for f being PartFunc of REAL,REAL
for a, b being Real st a < b & f is_differentiable_on_interval ['a,b'] holds
f is_differentiable_on ].a,b.[

proof end;

theorem :: FDIFF_12:8

for f being PartFunc of REAL,REAL
for a, b being Real st a <= b & f is_differentiable_on_interval ['a,b'] holds
( (f `\ ['a,b']) . a = Rdiff (f,a) & (f `\ ['a,b']) . b = Ldiff (f,b) & ( for x being Real st x in ].a,b.[ holds
(f `\ ['a,b']) . x = diff (f,x) ) )

proof end;

Lm7: for x, r being Real
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st r > 0 & rng c = {x} & ( for n being Nat holds h . n > 0 ) holds
ex N being Nat st
( rng ((h ^\ N) + c) c= ].x,(x + r).[ & ( for m being Nat holds ((h ^\ N) + c) . m = (h + c) . (N + m) ) & ( for m being Nat st N <= m holds
( |.(h . m).| < r & x < (h + c) . m & (h + c) . m < x + r ) ) )

proof end;

Lm8: for x, r being Real
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st r > 0 & rng c = {x} & ( for n being Nat holds h . n < 0 ) holds
ex N being Nat st
( rng ((h ^\ N) + c) c= ].(x - r),x.[ & ( for m being Nat holds ((h ^\ N) + c) . m = (h + c) . (N + m) ) & ( for m being Nat st N <= m holds
( |.(h . m).| < r & x - r < (h + c) . m & (h + c) . m < x ) ) )

proof end;

theorem Th9: :: FDIFF_12:9

for f being PartFunc of REAL,REAL
for I being Interval
for x being Real st f | I is_right_differentiable_in x holds
( f is_right_differentiable_in x & Rdiff ((f | I),x) = Rdiff (f,x) )

proof end;

theorem Th10: :: FDIFF_12:10

for f being PartFunc of REAL,REAL
for I being Interval
for x being Real st f | I is_left_differentiable_in x holds
( f is_left_differentiable_in x & Ldiff ((f | I),x) = Ldiff (f,x) )

proof end;

Lm9: for I being non empty Interval
for x being Real st inf I < x & x < sup I holds
ex Z being open Subset of REAL st
( x in Z & Z c= ].(inf I),(sup I).[ )

proof end;

theorem Th11: :: FDIFF_12:11

for f being PartFunc of REAL,REAL
for I being non empty Interval holds
( f is_differentiable_on_interval I iff ( I c= dom f & ( for x being Real st x in I holds
( ( x = inf I implies f | I is_right_differentiable_in x ) & ( x = sup I implies f | I is_left_differentiable_in x ) & ( x in ].(inf I),(sup I).[ implies f is_differentiable_in x ) ) ) ) )

proof end;

theorem :: FDIFF_12:12

for f being PartFunc of REAL,REAL
for I being non empty Interval st I is open_interval holds
( f is_differentiable_on I iff f is_differentiable_on_interval I )

proof end;

Lm10: for X being set st X is Subset of REAL holds
X is Subset of ExtREAL

proof end;

Lm11: for I being non empty Interval holds
( not inf I in I or I is closed_interval or I is right_open_interval )

proof end;

Lm12: for I being non empty Interval holds
( not sup I in I or I is closed_interval or I is left_open_interval )

proof end;

Lm13: for I being non empty Interval holds ].(inf I),(sup I).[ c= I
by Th2;

Lm14: for I being non empty Interval st inf I in I & inf I < sup I holds
ex e being Real st
( e > 0 & [.(lower_bound I),((lower_bound I) + e).] c= I )

proof end;

Lm15: for I being non empty Interval st sup I in I & inf I < sup I holds
ex e being Real st
( e > 0 & [.((upper_bound I) - e),(upper_bound I).] c= I )

proof end;

theorem :: FDIFF_12:13

for f being PartFunc of REAL,REAL
for x0, r being Real st f is_right_differentiable_in x0 & rng f = {r} holds
Rdiff (f,x0) = 0

proof end;

theorem :: FDIFF_12:14

for f being PartFunc of REAL,REAL
for x0, r being Real st f is_left_differentiable_in x0 & rng f = {r} holds
Ldiff (f,x0) = 0

proof end;

theorem Th15: :: FDIFF_12:15

for f being PartFunc of REAL,REAL
for I being non empty Interval st I c= dom f & inf I < sup I & ex r being Real st rng f = {r} holds
( f is_differentiable_on_interval I & ( for x being Real st x in I holds
(f `\ I) . x = 0 ) )

proof end;

theorem :: FDIFF_12:16

for f being PartFunc of REAL,REAL
for x0 being Real st dom f c= left_open_halfline x0 & f is_Lcontinuous_in x0 holds
f is_continuous_in x0

proof end;

theorem :: FDIFF_12:17

for f being PartFunc of REAL,REAL
for x0 being Real st dom f c= right_open_halfline x0 & f is_Rcontinuous_in x0 holds
f is_continuous_in x0

proof end;

theorem :: FDIFF_12:18

for f being PartFunc of REAL,REAL
for I being non empty Interval st I c= dom f & inf I < sup I & f | I = id I holds
( f is_differentiable_on_interval I & ( for x being Real st x in I holds
(f `\ I) . x = 1 ) )

proof end;

theorem :: FDIFF_12:19

for f1, f2 being PartFunc of REAL,REAL
for I being non empty Interval st I c= dom (f1 + f2) & f1 is_differentiable_on_interval I & f2 is_differentiable_on_interval I holds
( f1 + f2 is_differentiable_on_interval I & (f1 + f2) `\ I = (f1 `\ I) + (f2 `\ I) & ( for x being Real st x in I holds
((f1 + f2) `\ I) . x = ((f1 `\ I) . x) + ((f2 `\ I) . x) ) )

proof end;

theorem :: FDIFF_12:20

for f1, f2 being PartFunc of REAL,REAL
for I being non empty Interval st I c= dom (f1 - f2) & f1 is_differentiable_on_interval I & f2 is_differentiable_on_interval I holds
( f1 - f2 is_differentiable_on_interval I & (f1 - f2) `\ I = (f1 `\ I) - (f2 `\ I) & ( for x being Real st x in I holds
((f1 - f2) `\ I) . x = ((f1 `\ I) . x) - ((f2 `\ I) . x) ) )

proof end;

Lm16: for f being PartFunc of REAL,REAL
for x0 being Real st f is_right_differentiable_in x0 holds
( 0 (#) f is_right_differentiable_in x0 & Rdiff ((0 (#) f),x0) = 0 )

proof end;

Lm17: for f being PartFunc of REAL,REAL
for x0 being Real st f is_left_differentiable_in x0 holds
( 0 (#) f is_left_differentiable_in x0 & Ldiff ((0 (#) f),x0) = 0 )

proof end;

Lm18: for f being PartFunc of REAL,REAL
for x0, r being Real st r <> 0 & f is_right_differentiable_in x0 holds
( r (#) f is_right_differentiable_in x0 & Rdiff ((r (#) f),x0) = r * (Rdiff (f,x0)) )

proof end;

Lm19: for f being PartFunc of REAL,REAL
for x0, r being Real st r <> 0 & f is_left_differentiable_in x0 holds
( r (#) f is_left_differentiable_in x0 & Ldiff ((r (#) f),x0) = r * (Ldiff (f,x0)) )

proof end;

theorem Th21: :: FDIFF_12:21

for f being PartFunc of REAL,REAL
for x0, r being Real st f is_right_differentiable_in x0 holds
( r (#) f is_right_differentiable_in x0 & Rdiff ((r (#) f),x0) = r * (Rdiff (f,x0)) )

proof end;

theorem Th22: :: FDIFF_12:22

for f being PartFunc of REAL,REAL
for x0, r being Real st f is_left_differentiable_in x0 holds
( r (#) f is_left_differentiable_in x0 & Ldiff ((r (#) f),x0) = r * (Ldiff (f,x0)) )

proof end;

theorem :: FDIFF_12:23

for f being PartFunc of REAL,REAL
for I being non empty Interval
for r being Real st f is_differentiable_on_interval I holds
( r (#) f is_differentiable_on_interval I & (r (#) f) `\ I = r (#) (f `\ I) & ( for x being Real st x in I holds
((r (#) f) `\ I) . x = r * ((f `\ I) . x) ) )

proof end;

theorem :: FDIFF_12:24

for f1, f2 being PartFunc of REAL,REAL
for I being non empty Interval st f1 is_differentiable_on_interval I & f2 is_differentiable_on_interval I holds
( f1 (#) f2 is_differentiable_on_interval I & (f1 (#) f2) `\ I = (f2 (#) (f1 `\ I)) + (f1 (#) (f2 `\ I)) & ( for x being Real st x in I holds
((f1 (#) f2) `\ I) . x = ((f2 . x) * ((f1 `\ I) . x)) + ((f1 . x) * ((f2 `\ I) . x)) ) )

proof end;

theorem :: FDIFF_12:25

for f1, f2 being PartFunc of REAL,REAL
for I being non empty Interval st I c= dom (f1 / f2) & f1 is_differentiable_on_interval I & f2 is_differentiable_on_interval I holds
( f1 / f2 is_differentiable_on_interval I & (f1 / f2) `\ I = (((f1 `\ I) (#) f2) - ((f2 `\ I) (#) f1)) / (f2 ^2) & ( for x being Real st x in I holds
((f1 / f2) `\ I) . x = ((((f1 `\ I) . x) * (f2 . x)) - (((f2 `\ I) . x) * (f1 . x))) / ((f2 . x) ^2) ) )

proof end;

theorem :: FDIFF_12:26

for f being PartFunc of REAL,REAL
for x0 being Real st x0 in dom f & f is_continuous_in x0 holds
( f is_Lcontinuous_in x0 & f is_Rcontinuous_in x0 )

proof end;

theorem Th27: :: FDIFF_12:27

for x0 being Real
for f being PartFunc of REAL,REAL holds
( f is_Lcontinuous_in x0 iff ( x0 in dom f & ( for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x being Real st x in dom f & x0 - d < x & x < x0 holds
|.((f . x) - (f . x0)).| < e ) ) ) ) )

proof end;

theorem Th28: :: FDIFF_12:28

for x0 being Real
for f being PartFunc of REAL,REAL holds
( f is_Rcontinuous_in x0 iff ( x0 in dom f & ( for e being Real st 0 < e holds
ex d being Real st
( 0 < d & ( for x being Real st x in dom f & x0 < x & x < x0 + d holds
|.((f . x) - (f . x0)).| < e ) ) ) ) )

proof end;

theorem :: FDIFF_12:29

for f being PartFunc of REAL,REAL
for x0 being Real st f is_Lcontinuous_in x0 & f is_Rcontinuous_in x0 holds
f is_continuous_in x0

proof end;

theorem :: FDIFF_12:30

for x0 being Real
for f being PartFunc of REAL,REAL st f is_Lcontinuous_in x0 & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ) holds
( f is_left_convergent_in x0 & lim_left (f,x0) = f . x0 )

proof end;

theorem :: FDIFF_12:31

for x0 being Real
for f being PartFunc of REAL,REAL st f is_Rcontinuous_in x0 & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ) holds
( f is_right_convergent_in x0 & lim_right (f,x0) = f . x0 )

proof end;

theorem :: FDIFF_12:32

for f being PartFunc of REAL,REAL
for x0 being Real st x0 in dom f & f is_right_convergent_in x0 & lim_right (f,x0) = f . x0 holds
f is_Rcontinuous_in x0

proof end;

theorem :: FDIFF_12:33

for x0 being Real
for f being PartFunc of REAL,REAL st x0 in dom f & f is_left_convergent_in x0 & lim_left (f,x0) = f . x0 holds
f is_Lcontinuous_in x0

proof end;

theorem :: FDIFF_12:34

for f being PartFunc of REAL,REAL
for x0 being Real st f is_convergent_in x0 & lim (f,x0) = f . x0 holds
f is_continuous_in x0

proof end;

theorem Th35: :: FDIFF_12:35

for f being PartFunc of REAL,REAL
for x0 being Real st f is_Rcontinuous_in x0 holds
f | (right_closed_halfline x0) is_continuous_in x0

proof end;

theorem Th36: :: FDIFF_12:36

for f being PartFunc of REAL,REAL
for x0 being Real st f is_Lcontinuous_in x0 holds
f | (left_closed_halfline x0) is_continuous_in x0

proof end;

theorem :: FDIFF_12:37

for f being PartFunc of REAL,REAL
for I being non empty Interval st f is_differentiable_on_interval I holds
f | I is continuous

proof end;

theorem :: FDIFF_12:38

for f being PartFunc of REAL,REAL
for I, J being non empty Interval st f is_differentiable_on_interval I & J c= I & inf J < sup J holds
( f is_differentiable_on_interval J & ( for x being Real st x in J holds
(f `\ I) . x = (f `\ J) . x ) )

proof end;

theorem :: FDIFF_12:39

for f being PartFunc of REAL,REAL
for Z being open Subset of REAL
for I being non empty Interval st I c= Z & inf I < sup I & f is_differentiable_on Z holds
f is_differentiable_on_interval I

proof end;

Lm20: for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_right_differentiable_in x0 & f2 is_differentiable_in f1 . x0 holds
ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom (f2 * f1) )

proof end;

theorem Th40: :: FDIFF_12:40

for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_right_differentiable_in x0 & f2 is_differentiable_in f1 . x0 holds
( f2 * f1 is_right_differentiable_in x0 & Rdiff ((f2 * f1),x0) = (diff (f2,(f1 . x0))) * (Rdiff (f1,x0)) )

proof end;

Lm21: for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_left_differentiable_in x0 & f2 is_differentiable_in f1 . x0 holds
ex r being Real st
( r > 0 & [.(x0 - r),x0.] c= dom (f2 * f1) )

proof end;

theorem Th41: :: FDIFF_12:41

for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_left_differentiable_in x0 & f2 is_differentiable_in f1 . x0 holds
( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (diff (f2,(f1 . x0))) * (Ldiff (f1,x0)) )

proof end;

theorem Th42: :: FDIFF_12:42

for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in f1 . x0 & ( for r1 being Real st r1 > 0 holds
ex r0 being Real st
( r0 > 0 & [.x0,(x0 + r0).] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) ) ) holds
( f2 * f1 is_right_differentiable_in x0 & Rdiff ((f2 * f1),x0) = (Rdiff (f2,(f1 . x0))) * (Rdiff (f1,x0)) )

proof end;

theorem Th43: :: FDIFF_12:43

for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_left_differentiable_in x0 & f2 is_right_differentiable_in f1 . x0 & ( for r1 being Real st r1 > 0 holds
ex r0 being Real st
( r0 > 0 & [.(x0 - r0),x0.] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) ) ) holds
( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) )

proof end;

theorem Th44: :: FDIFF_12:44

for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_in x0 & f2 is_right_differentiable_in f1 . x0 & ( for r1 being Real st r1 > 0 holds
ex r0 being Real st
( r0 > 0 & [.(x0 - r0),(x0 + r0).] c= dom ([.(f1 . x0),((f1 . x0) + r1).] |` f1) ) ) holds
( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (Rdiff (f2,(f1 . x0))) * (diff (f1,x0)) )

proof end;

theorem Th45: :: FDIFF_12:45

for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_right_differentiable_in x0 & f2 is_left_differentiable_in f1 . x0 & ( for r1 being Real st r1 > 0 holds
ex r0 being Real st
( r0 > 0 & [.x0,(x0 + r0).] c= dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1) ) ) holds
( f2 * f1 is_right_differentiable_in x0 & Rdiff ((f2 * f1),x0) = (Ldiff (f2,(f1 . x0))) * (Rdiff (f1,x0)) )

proof end;

theorem Th46: :: FDIFF_12:46

for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in f1 . x0 & ( for r1 being Real st r1 > 0 holds
ex r0 being Real st
( r0 > 0 & [.(x0 - r0),x0.] c= dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1) ) ) holds
( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (Ldiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) )

proof end;

theorem Th47: :: FDIFF_12:47

for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_in x0 & f2 is_left_differentiable_in f1 . x0 & ( for r1 being Real st r1 > 0 holds
ex r0 being Real st
( r0 > 0 & [.(x0 - r0),(x0 + r0).] c= dom ([.((f1 . x0) - r1),(f1 . x0).] |` f1) ) ) holds
( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (Ldiff (f2,(f1 . x0))) * (diff (f1,x0)) )

proof end;

theorem :: FDIFF_12:48

for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_right_differentiable_in x0 & f2 is_right_differentiable_in f1 . x0 & ex r being Real st
( r > 0 & f1 | [.x0,(x0 + r).] is non-decreasing ) holds
( f2 * f1 is_right_differentiable_in x0 & Rdiff ((f2 * f1),x0) = (Rdiff (f2,(f1 . x0))) * (Rdiff (f1,x0)) )

proof end;

theorem :: FDIFF_12:49

for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_left_differentiable_in x0 & f2 is_right_differentiable_in f1 . x0 & ex r being Real st
( r > 0 & f1 | [.(x0 - r),x0.] is non-increasing ) holds
( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (Rdiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) )

proof end;

theorem :: FDIFF_12:50

for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_right_differentiable_in x0 & f2 is_left_differentiable_in f1 . x0 & ex r being Real st
( r > 0 & f1 | [.x0,(x0 + r).] is non-increasing ) holds
( f2 * f1 is_right_differentiable_in x0 & Rdiff ((f2 * f1),x0) = (Ldiff (f2,(f1 . x0))) * (Rdiff (f1,x0)) )

proof end;

theorem :: FDIFF_12:51

for x0 being Real
for f1, f2 being PartFunc of REAL,REAL st f1 is_left_differentiable_in x0 & f2 is_left_differentiable_in f1 . x0 & ex r being Real st
( r > 0 & f1 | [.(x0 - r),x0.] is non-decreasing ) holds
( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (Ldiff (f2,(f1 . x0))) * (Ldiff (f1,x0)) )

proof end;

Lm22: for I being non empty Interval holds
( I = [.(inf I),(sup I).] or I = ].(inf I),(sup I).] or I = [.(inf I),(sup I).[ or I = ].(inf I),(sup I).[ )

proof end;

Lm23: for I being non empty Interval holds
( not inf I in I or I = [.(inf I),(sup I).] or I = [.(inf I),(sup I).[ )

proof end;

Lm24: for I being non empty Interval holds
( not sup I in I or I = [.(inf I),(sup I).] or I = ].(inf I),(sup I).] )

proof end;

Lm25: for I being non empty Interval st not sup I in I & not inf I in I holds
I = ].(inf I),(sup I).[

proof end;

Lm26: for x0 being Real
for f1, f2 being PartFunc of REAL,REAL
for I, J being non empty Interval st f1 is_differentiable_on_interval I & f2 is_differentiable_on_interval J & f1 .: I c= J & x0 = inf I & x0 in I holds
( f2 * f1 is_right_differentiable_in x0 & Rdiff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )

proof end;

Lm27: for x0 being Real
for f1, f2 being PartFunc of REAL,REAL
for I, J being non empty Interval st f1 is_differentiable_on_interval I & f2 is_differentiable_on_interval J & f1 .: I c= J & x0 = sup I & x0 in I holds
( f2 * f1 is_left_differentiable_in x0 & Ldiff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )

proof end;

Lm28: for x0 being Real
for f1, f2 being PartFunc of REAL,REAL
for I, J being non empty Interval st f1 is_differentiable_on_interval I & f2 is_differentiable_on_interval J & f1 .: I c= J & x0 in ].(inf I),(sup I).[ & x0 in I holds
( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (((f2 `\ J) * f1) (#) (f1 `\ I)) . x0 )

proof end;

theorem :: FDIFF_12:52

for f1, f2 being PartFunc of REAL,REAL
for I, J being non empty Interval st f1 is_differentiable_on_interval I & f2 is_differentiable_on_interval J & f1 .: I c= J holds
( f2 * f1 is_differentiable_on_interval I & (f2 * f1) `\ I = ((f2 `\ J) * f1) (#) (f1 `\ I) )

proof end;