:: by Junjie Zhao , Xiquan Liang and Li Yan

::

:: Received March 18, 2008

:: Copyright (c) 2008-2016 Association of Mizar Users

theorem :: HFDIFF_1:4

for r, p being Real

for n being Element of NAT holds (r * p) (#) ((#Z n) ^) = r (#) (p (#) ((#Z n) ^))

for n being Element of NAT holds (r * p) (#) ((#Z n) ^) = r (#) (p (#) ((#Z n) ^))

proof end;

theorem Th5: :: HFDIFF_1:5

for f1 being PartFunc of REAL,REAL

for n, m being Real holds (n (#) f1) + (m (#) f1) = (n + m) (#) f1

for n, m being Real holds (n (#) f1) + (m (#) f1) = (n + m) (#) f1

proof end;

theorem Th6: :: HFDIFF_1:6

for Z being open Subset of REAL

for f being PartFunc of REAL,REAL st f | Z is_differentiable_on Z holds

f is_differentiable_on Z

for f being PartFunc of REAL,REAL st f | Z is_differentiable_on Z holds

f is_differentiable_on Z

proof end;

theorem Th7: :: HFDIFF_1:7

for n being Element of NAT

for Z being open Subset of REAL

for f1 being PartFunc of REAL,REAL st n >= 1 & f1 is_differentiable_on n,Z holds

f1 is_differentiable_on Z

for Z being open Subset of REAL

for f1 being PartFunc of REAL,REAL st n >= 1 & f1 is_differentiable_on n,Z holds

f1 is_differentiable_on Z

proof end;

:: 1 f.x = sin.x

theorem :: HFDIFF_1:9

for x being Real

for Z being open Subset of REAL st x in Z holds

((diff (sin,Z)) . 2) . x = - (sin . x)

for Z being open Subset of REAL st x in Z holds

((diff (sin,Z)) . 2) . x = - (sin . x)

proof end;

theorem :: HFDIFF_1:10

for x being Real

for Z being open Subset of REAL st x in Z holds

((diff (sin,Z)) . 3) . x = (- cos) . x

for Z being open Subset of REAL st x in Z holds

((diff (sin,Z)) . 3) . x = (- cos) . x

proof end;

theorem Th11: :: HFDIFF_1:11

for x being Real

for n being Element of NAT

for Z being open Subset of REAL st x in Z holds

((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2))

for n being Element of NAT

for Z being open Subset of REAL st x in Z holds

((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2))

proof end;

:: 2 f.x = cos.x

theorem :: HFDIFF_1:12

for x being Real

for Z being open Subset of REAL st x in Z holds

((diff (cos,Z)) . 2) . x = - (cos . x)

for Z being open Subset of REAL st x in Z holds

((diff (cos,Z)) . 2) . x = - (cos . x)

proof end;

theorem Th14: :: HFDIFF_1:14

for x being Real

for n being Element of NAT

for Z being open Subset of REAL st x in Z holds

((diff (cos,Z)) . n) . x = cos . (x + ((n * PI) / 2))

for n being Element of NAT

for Z being open Subset of REAL st x in Z holds

((diff (cos,Z)) . n) . x = cos . (x + ((n * PI) / 2))

proof end;

theorem Th15: :: HFDIFF_1:15

for n being Element of NAT

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds

(diff ((f1 + f2),Z)) . n = ((diff (f1,Z)) . n) + ((diff (f2,Z)) . n)

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds

(diff ((f1 + f2),Z)) . n = ((diff (f1,Z)) . n) + ((diff (f2,Z)) . n)

proof end;

theorem Th16: :: HFDIFF_1:16

for n being Element of NAT

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds

(diff ((f1 - f2),Z)) . n = ((diff (f1,Z)) . n) - ((diff (f2,Z)) . n)

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds

(diff ((f1 - f2),Z)) . n = ((diff (f1,Z)) . n) - ((diff (f2,Z)) . n)

proof end;

theorem Th17: :: HFDIFF_1:17

for n, i being Element of NAT

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z & i <= n holds

(diff ((f1 + f2),Z)) . i = ((diff (f1,Z)) . i) + ((diff (f2,Z)) . i)

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z & i <= n holds

(diff ((f1 + f2),Z)) . i = ((diff (f1,Z)) . i) + ((diff (f2,Z)) . i)

proof end;

theorem Th18: :: HFDIFF_1:18

for n, i being Element of NAT

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z & i <= n holds

(diff ((f1 - f2),Z)) . i = ((diff (f1,Z)) . i) - ((diff (f2,Z)) . i)

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z & i <= n holds

(diff ((f1 - f2),Z)) . i = ((diff (f1,Z)) . i) - ((diff (f2,Z)) . i)

proof end;

theorem :: HFDIFF_1:19

for n being Element of NAT

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds

f1 + f2 is_differentiable_on n,Z

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds

f1 + f2 is_differentiable_on n,Z

proof end;

theorem :: HFDIFF_1:20

for n being Element of NAT

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds

f1 - f2 is_differentiable_on n,Z

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds

f1 - f2 is_differentiable_on n,Z

proof end;

theorem Th21: :: HFDIFF_1:21

for r being Real

for n being Element of NAT

for Z being open Subset of REAL

for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds

(diff ((r (#) f),Z)) . n = r (#) ((diff (f,Z)) . n)

for n being Element of NAT

for Z being open Subset of REAL

for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds

(diff ((r (#) f),Z)) . n = r (#) ((diff (f,Z)) . n)

proof end;

theorem Th22: :: HFDIFF_1:22

for r being Real

for n being Element of NAT

for Z being open Subset of REAL

for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds

r (#) f is_differentiable_on n,Z

for n being Element of NAT

for Z being open Subset of REAL

for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds

r (#) f is_differentiable_on n,Z

proof end;

theorem :: HFDIFF_1:23

for Z being open Subset of REAL

for f being PartFunc of REAL,REAL st f is_differentiable_on Z holds

(diff (f,Z)) . 1 = f `| Z

for f being PartFunc of REAL,REAL st f is_differentiable_on Z holds

(diff (f,Z)) . 1 = f `| Z

proof end;

theorem :: HFDIFF_1:24

for n being Element of NAT

for Z being open Subset of REAL

for f1 being PartFunc of REAL,REAL st n >= 1 & f1 is_differentiable_on n,Z holds

(diff (f1,Z)) . 1 = f1 `| Z

for Z being open Subset of REAL

for f1 being PartFunc of REAL,REAL st n >= 1 & f1 is_differentiable_on n,Z holds

(diff (f1,Z)) . 1 = f1 `| Z

proof end;

theorem :: HFDIFF_1:25

for x, r being Real

for n being Element of NAT

for Z being open Subset of REAL st x in Z holds

((diff ((r (#) sin),Z)) . n) . x = r * (sin . (x + ((n * PI) / 2)))

for n being Element of NAT

for Z being open Subset of REAL st x in Z holds

((diff ((r (#) sin),Z)) . n) . x = r * (sin . (x + ((n * PI) / 2)))

proof end;

theorem :: HFDIFF_1:26

for x, r being Real

for n being Element of NAT

for Z being open Subset of REAL st x in Z holds

((diff ((r (#) cos),Z)) . n) . x = r * (cos . (x + ((n * PI) / 2)))

for n being Element of NAT

for Z being open Subset of REAL st x in Z holds

((diff ((r (#) cos),Z)) . n) . x = r * (cos . (x + ((n * PI) / 2)))

proof end;

theorem :: HFDIFF_1:27

for x, r being Real

for n being Element of NAT

for Z being open Subset of REAL st x in Z holds

((diff ((r (#) exp_R),Z)) . n) . x = r * (exp_R . x)

for n being Element of NAT

for Z being open Subset of REAL st x in Z holds

((diff ((r (#) exp_R),Z)) . n) . x = r * (exp_R . x)

proof end;

theorem Th28: :: HFDIFF_1:28

for n being Element of NAT

for Z being open Subset of REAL holds (#Z n) `| Z = (n (#) (#Z (n - 1))) | Z

for Z being open Subset of REAL holds (#Z n) `| Z = (n (#) (#Z (n - 1))) | Z

proof end;

theorem Th29: :: HFDIFF_1:29

for x being Real

for n being Element of NAT st x <> 0 holds

( (#Z n) ^ is_differentiable_in x & diff (((#Z n) ^),x) = - ((n * (x #Z (n - 1))) / ((x #Z n) ^2)) )

for n being Element of NAT st x <> 0 holds

( (#Z n) ^ is_differentiable_in x & diff (((#Z n) ^),x) = - ((n * (x #Z (n - 1))) / ((x #Z n) ^2)) )

proof end;

theorem Th30: :: HFDIFF_1:30

for n being Element of NAT

for Z being open Subset of REAL st n >= 1 holds

(diff ((#Z n),Z)) . 2 = ((n * (n - 1)) (#) (#Z (n - 2))) | Z

for Z being open Subset of REAL st n >= 1 holds

(diff ((#Z n),Z)) . 2 = ((n * (n - 1)) (#) (#Z (n - 2))) | Z

proof end;

theorem :: HFDIFF_1:31

for n being Element of NAT

for Z being open Subset of REAL st n >= 2 holds

(diff ((#Z n),Z)) . 3 = (((n * (n - 1)) * (n - 2)) (#) (#Z (n - 3))) | Z

for Z being open Subset of REAL st n >= 2 holds

(diff ((#Z n),Z)) . 3 = (((n * (n - 1)) * (n - 2)) (#) (#Z (n - 3))) | Z

proof end;

Lm1: for n, m being Element of NAT st n > 1 holds

((m !) / (n !)) * n = (m !) / ((n -' 1) !)

proof end;

theorem Th32: :: HFDIFF_1:32

for n, m being Element of NAT

for Z being open Subset of REAL st n > m holds

(diff ((#Z n),Z)) . m = (((n choose m) * (m !)) (#) (#Z (n - m))) | Z

for Z being open Subset of REAL st n > m holds

(diff ((#Z n),Z)) . m = (((n choose m) * (m !)) (#) (#Z (n - m))) | Z

proof end;

theorem :: HFDIFF_1:33

theorem :: HFDIFF_1:34

for x, x0 being Real

for n being Element of NAT

for Z being open Subset of REAL st x0 in Z holds

( (Taylor (sin,Z,x0,x)) . n = ((sin . (x0 + ((n * PI) / 2))) * ((x - x0) |^ n)) / (n !) & (Taylor (cos,Z,x0,x)) . n = ((cos . (x0 + ((n * PI) / 2))) * ((x - x0) |^ n)) / (n !) )

for n being Element of NAT

for Z being open Subset of REAL st x0 in Z holds

( (Taylor (sin,Z,x0,x)) . n = ((sin . (x0 + ((n * PI) / 2))) * ((x - x0) |^ n)) / (n !) & (Taylor (cos,Z,x0,x)) . n = ((cos . (x0 + ((n * PI) / 2))) * ((x - x0) |^ n)) / (n !) )

proof end;

theorem :: HFDIFF_1:35

for x, r being Real

for n being Element of NAT st r > 0 holds

( (Maclaurin (sin,].(- r),r.[,x)) . n = ((sin . ((n * PI) / 2)) * (x |^ n)) / (n !) & (Maclaurin (cos,].(- r),r.[,x)) . n = ((cos . ((n * PI) / 2)) * (x |^ n)) / (n !) )

for n being Element of NAT st r > 0 holds

( (Maclaurin (sin,].(- r),r.[,x)) . n = ((sin . ((n * PI) / 2)) * (x |^ n)) / (n !) & (Maclaurin (cos,].(- r),r.[,x)) . n = ((cos . ((n * PI) / 2)) * (x |^ n)) / (n !) )

proof end;

theorem Th36: :: HFDIFF_1:36

for x being Real

for n, m being Element of NAT

for Z being open Subset of REAL st n > m & x in Z holds

((diff ((#Z n),Z)) . m) . x = ((n choose m) * (m !)) * (x #Z (n - m))

for n, m being Element of NAT

for Z being open Subset of REAL st n > m & x in Z holds

((diff ((#Z n),Z)) . m) . x = ((n choose m) * (m !)) * (x #Z (n - m))

proof end;

theorem Th37: :: HFDIFF_1:37

for x being Real

for m being Element of NAT

for Z being open Subset of REAL st x in Z holds

((diff ((#Z m),Z)) . m) . x = m !

for m being Element of NAT

for Z being open Subset of REAL st x in Z holds

((diff ((#Z m),Z)) . m) . x = m !

proof end;

theorem :: HFDIFF_1:39

for x, a being Real

for n, m being Element of NAT

for Z being open Subset of REAL st x in Z & n > m holds

((diff ((a (#) (#Z n)),Z)) . m) . x = ((a * (n choose m)) * (m !)) * (x #Z (n - m))

for n, m being Element of NAT

for Z being open Subset of REAL st x in Z & n > m holds

((diff ((a (#) (#Z n)),Z)) . m) . x = ((a * (n choose m)) * (m !)) * (x #Z (n - m))

proof end;

theorem :: HFDIFF_1:40

for x, a being Real

for n being Element of NAT

for Z being open Subset of REAL st x in Z holds

((diff ((a (#) (#Z n)),Z)) . n) . x = a * (n !)

for n being Element of NAT

for Z being open Subset of REAL st x in Z holds

((diff ((a (#) (#Z n)),Z)) . n) . x = a * (n !)

proof end;

theorem Th41: :: HFDIFF_1:41

for x, x0 being Real

for n, m being Element of NAT

for Z being open Subset of REAL st x0 in Z & n > m holds

( (Taylor ((#Z n),Z,x0,x)) . m = ((n choose m) * (x0 #Z (n - m))) * ((x - x0) |^ m) & (Taylor ((#Z n),Z,x0,x)) . n = (x - x0) |^ n )

for n, m being Element of NAT

for Z being open Subset of REAL st x0 in Z & n > m holds

( (Taylor ((#Z n),Z,x0,x)) . m = ((n choose m) * (x0 #Z (n - m))) * ((x - x0) |^ m) & (Taylor ((#Z n),Z,x0,x)) . n = (x - x0) |^ n )

proof end;

theorem :: HFDIFF_1:42

for n, m being Element of NAT

for r, x being Element of REAL st n > m & r > 0 holds

( (Maclaurin ((#Z n),].(- r),r.[,x)) . m = 0 & (Maclaurin ((#Z n),].(- r),r.[,x)) . n = x |^ n )

for r, x being Element of REAL st n > m & r > 0 holds

( (Maclaurin ((#Z n),].(- r),r.[,x)) . m = 0 & (Maclaurin ((#Z n),].(- r),r.[,x)) . n = x |^ n )

proof end;

theorem Th43: :: HFDIFF_1:43

for n being Element of NAT

for Z being open Subset of REAL st not 0 in Z holds

(#Z n) ^ is_differentiable_on Z

for Z being open Subset of REAL st not 0 in Z holds

(#Z n) ^ is_differentiable_on Z

proof end;

theorem :: HFDIFF_1:44

for x0 being Real

for n being Element of NAT

for Z being open Subset of REAL st not 0 in Z & x0 in Z holds

(((#Z n) ^) `| Z) . x0 = - (n / ((#Z (n + 1)) . x0))

for n being Element of NAT

for Z being open Subset of REAL st not 0 in Z & x0 in Z holds

(((#Z n) ^) `| Z) . x0 = - (n / ((#Z (n + 1)) . x0))

proof end;

Lm2: #Z 1 = id REAL

proof end;

theorem Th45: :: HFDIFF_1:45

for x being Real st x <> 0 holds

( (id REAL) ^ is_differentiable_in x & diff (((id REAL) ^),x) = - (1 / (x ^2)) )

( (id REAL) ^ is_differentiable_in x & diff (((id REAL) ^),x) = - (1 / (x ^2)) )

proof end;

theorem Th47: :: HFDIFF_1:47

for x being Real st x <> 0 holds

( (#Z 2) ^ is_differentiable_in x & diff (((#Z 2) ^),x) = - ((2 * x) / ((x #Z 2) ^2)) )

( (#Z 2) ^ is_differentiable_in x & diff (((#Z 2) ^),x) = - ((2 * x) / ((x #Z 2) ^2)) )

proof end;

theorem Th49: :: HFDIFF_1:49

for n being Element of NAT

for Z being open Subset of REAL st not 0 in Z & n >= 1 holds

((#Z n) ^) `| Z = ((- n) (#) ((#Z (n + 1)) ^)) | Z

for Z being open Subset of REAL st not 0 in Z & n >= 1 holds

((#Z n) ^) `| Z = ((- n) (#) ((#Z (n + 1)) ^)) | Z

proof end;

theorem Th50: :: HFDIFF_1:50

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on 2,Z & f2 is_differentiable_on 2,Z holds

(diff ((f1 (#) f2),Z)) . 2 = ((((diff (f1,Z)) . 2) (#) f2) + (2 (#) ((f1 `| Z) (#) (f2 `| Z)))) + (f1 (#) ((diff (f2,Z)) . 2))

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on 2,Z & f2 is_differentiable_on 2,Z holds

(diff ((f1 (#) f2),Z)) . 2 = ((((diff (f1,Z)) . 2) (#) f2) + (2 (#) ((f1 `| Z) (#) (f2 `| Z)))) + (f1 (#) ((diff (f2,Z)) . 2))

proof end;

theorem :: HFDIFF_1:51

for Z being open Subset of REAL st Z c= dom ln & Z c= dom ((id REAL) ^) holds

ln `| Z = ((id REAL) ^) | Z

ln `| Z = ((id REAL) ^) | Z

proof end;

theorem :: HFDIFF_1:52

for x0 being Real

for n being Element of NAT

for Z being open Subset of REAL st n >= 1 & x0 in Z & not 0 in Z holds

((diff (((#Z n) ^),Z)) . 2) . x0 = (n * (n + 1)) * (((#Z (n + 2)) ^) . x0)

for n being Element of NAT

for Z being open Subset of REAL st n >= 1 & x0 in Z & not 0 in Z holds

((diff (((#Z n) ^),Z)) . 2) . x0 = (n * (n + 1)) * (((#Z (n + 2)) ^) . x0)

proof end;

theorem :: HFDIFF_1:53

for Z being open Subset of REAL holds (diff ((sin ^2),Z)) . 2 = (2 (#) ((cos ^2) | Z)) + ((- 2) (#) ((sin ^2) | Z))

proof end;

theorem :: HFDIFF_1:54

for Z being open Subset of REAL holds (diff ((cos ^2),Z)) . 2 = (2 (#) ((sin ^2) | Z)) + ((- 2) (#) ((cos ^2) | Z))

proof end;

theorem Th56: :: HFDIFF_1:56

for Z being open Subset of REAL st Z c= dom tan holds

( tan is_differentiable_on Z & tan `| Z = ((cos ^) ^2) | Z )

( tan is_differentiable_on Z & tan `| Z = ((cos ^) ^2) | Z )

proof end;

theorem Th57: :: HFDIFF_1:57

for Z being open Subset of REAL st Z c= dom tan holds

( cos ^ is_differentiable_on Z & (cos ^) `| Z = ((cos ^) (#) tan) | Z )

( cos ^ is_differentiable_on Z & (cos ^) `| Z = ((cos ^) (#) tan) | Z )

proof end;

theorem :: HFDIFF_1:58

for Z being open Subset of REAL st Z c= dom tan holds

(diff (tan,Z)) . 2 = 2 (#) (((tan (#) (cos ^)) (#) (cos ^)) | Z)

(diff (tan,Z)) . 2 = 2 (#) (((tan (#) (cos ^)) (#) (cos ^)) | Z)

proof end;

theorem Th59: :: HFDIFF_1:59

for Z being open Subset of REAL st Z c= dom cot holds

( cot is_differentiable_on Z & cot `| Z = ((- 1) (#) ((sin ^) ^2)) | Z )

( cot is_differentiable_on Z & cot `| Z = ((- 1) (#) ((sin ^) ^2)) | Z )

proof end;

theorem Th60: :: HFDIFF_1:60

for Z being open Subset of REAL st Z c= dom cot holds

( sin ^ is_differentiable_on Z & (sin ^) `| Z = (- ((sin ^) (#) cot)) | Z )

( sin ^ is_differentiable_on Z & (sin ^) `| Z = (- ((sin ^) (#) cot)) | Z )

proof end;

theorem :: HFDIFF_1:61

for Z being open Subset of REAL st Z c= dom cot holds

(diff (cot,Z)) . 2 = 2 (#) (((cot (#) (sin ^)) (#) (sin ^)) | Z)

(diff (cot,Z)) . 2 = 2 (#) (((cot (#) (sin ^)) (#) (sin ^)) | Z)

proof end;

theorem :: HFDIFF_1:63

for Z being open Subset of REAL holds (diff ((exp_R (#) cos),Z)) . 2 = 2 (#) ((exp_R (#) (- sin)) | Z)

proof end;

Lm3: for Z being open Subset of REAL

for f being PartFunc of REAL,REAL st f is_differentiable_on Z holds

(f `| Z) `| Z = (diff (f,Z)) . 2

proof end;

theorem Th64: :: HFDIFF_1:64

for Z being open Subset of REAL

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on 3,Z & f2 is_differentiable_on 3,Z holds

(diff ((f1 (#) f2),Z)) . 3 = ((((diff (f1,Z)) . 3) (#) f2) + ((3 (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (3 (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2))))) + (f1 (#) ((diff (f2,Z)) . 3))

for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on 3,Z & f2 is_differentiable_on 3,Z holds

(diff ((f1 (#) f2),Z)) . 3 = ((((diff (f1,Z)) . 3) (#) f2) + ((3 (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (3 (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2))))) + (f1 (#) ((diff (f2,Z)) . 3))

proof end;

theorem :: HFDIFF_1:66

for Z being open Subset of REAL

for f being PartFunc of REAL,REAL st f is_differentiable_on 2,Z holds

(diff ((f ^2),Z)) . 2 = (2 (#) (f (#) ((diff (f,Z)) . 2))) + (2 (#) ((f `| Z) ^2))

for f being PartFunc of REAL,REAL st f is_differentiable_on 2,Z holds

(diff ((f ^2),Z)) . 2 = (2 (#) (f (#) ((diff (f,Z)) . 2))) + (2 (#) ((f `| Z) ^2))

proof end;

Lm4: for f being PartFunc of REAL,REAL holds f / f = ((dom f) \ (f " {0})) --> 1

proof end;

Lm5: for f being PartFunc of REAL,REAL holds (f (#) (f (#) f)) " {0} = f " {0}

proof end;

theorem :: HFDIFF_1:67

for Z being open Subset of REAL

for f being PartFunc of REAL,REAL st f is_differentiable_on 2,Z & ( for x0 being Real st x0 in Z holds

f . x0 <> 0 ) holds

(diff ((f ^),Z)) . 2 = (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))

for f being PartFunc of REAL,REAL st f is_differentiable_on 2,Z & ( for x0 being Real st x0 in Z holds

f . x0 <> 0 ) holds

(diff ((f ^),Z)) . 2 = (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))

proof end;

theorem :: HFDIFF_1:68

for Z being open Subset of REAL holds (diff ((exp_R (#) sin),Z)) . 3 = (2 (#) (exp_R (#) ((- sin) + cos))) | Z

proof end;