:: Difference and Difference Quotient -- Part {III}
:: by Xiquan Liang and Ling Tang
::
:: Received November 17, 2009
:: Copyright (c) 2009-2012 Association of Mizar Users


begin

theorem Th1: :: DIFF_3:1
for h, x being Real
for f being Function of REAL,REAL holds (cD (f,h)) . x = ((fD (f,(h / 2))) . x) - ((fD (f,(- (h / 2)))) . x)
proofend;

theorem Th2: :: DIFF_3:2
for h, x being Real
for f being Function of REAL,REAL holds (fD (f,(- (h / 2)))) . x = - ((bD (f,(h / 2))) . x)
proofend;

theorem :: DIFF_3:3
for h, x being Real
for f being Function of REAL,REAL holds (cD (f,h)) . x = ((bD (f,(h / 2))) . x) - ((bD (f,(- (h / 2)))) . x)
proofend;

theorem :: DIFF_3:4
for n being Element of NAT
for r, h, x being Real
for f1, f2 being Function of REAL,REAL holds ((fdif (((r (#) f1) + f2),h)) . (n + 1)) . x = (r * (((fdif (f1,h)) . (n + 1)) . x)) + (((fdif (f2,h)) . (n + 1)) . x)
proofend;

theorem :: DIFF_3:5
for n being Element of NAT
for r, h, x being Real
for f1, f2 being Function of REAL,REAL holds ((fdif ((f1 + (r (#) f2)),h)) . (n + 1)) . x = (((fdif (f1,h)) . (n + 1)) . x) + (r * (((fdif (f2,h)) . (n + 1)) . x))
proofend;

theorem :: DIFF_3:6
for n being Element of NAT
for r1, r2, h, x being Real
for f1, f2 being Function of REAL,REAL holds ((fdif (((r1 (#) f1) - (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((fdif (f1,h)) . (n + 1)) . x)) - (r2 * (((fdif (f2,h)) . (n + 1)) . x))
proofend;

theorem :: DIFF_3:7
for h being Real
for f being Function of REAL,REAL holds (fdif (f,h)) . 1 = fD (f,h)
proofend;

theorem :: DIFF_3:8
for n being Element of NAT
for r, h, x being Real
for f1, f2 being Function of REAL,REAL holds ((bdif (((r (#) f1) + f2),h)) . (n + 1)) . x = (r * (((bdif (f1,h)) . (n + 1)) . x)) + (((bdif (f2,h)) . (n + 1)) . x)
proofend;

theorem :: DIFF_3:9
for n being Element of NAT
for r, h, x being Real
for f1, f2 being Function of REAL,REAL holds ((bdif ((f1 + (r (#) f2)),h)) . (n + 1)) . x = (((bdif (f1,h)) . (n + 1)) . x) + (r * (((bdif (f2,h)) . (n + 1)) . x))
proofend;

theorem :: DIFF_3:10
for n being Element of NAT
for r1, r2, h, x being Real
for f1, f2 being Function of REAL,REAL holds ((bdif (((r1 (#) f1) - (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((bdif (f1,h)) . (n + 1)) . x)) - (r2 * (((bdif (f2,h)) . (n + 1)) . x))
proofend;

theorem Th11: :: DIFF_3:11
for h being Real
for f being Function of REAL,REAL holds (bdif (f,h)) . 1 = bD (f,h)
proofend;

theorem :: DIFF_3:12
for m, n being Element of NAT
for h, x being Real
for f being Function of REAL,REAL holds ((bdif (((bdif (f,h)) . m),h)) . n) . x = ((bdif (f,h)) . (m + n)) . x
proofend;

theorem :: DIFF_3:13
for n being Element of NAT
for r, h, x being Real
for f1, f2 being Function of REAL,REAL holds ((cdif (((r (#) f1) + f2),h)) . (n + 1)) . x = (r * (((cdif (f1,h)) . (n + 1)) . x)) + (((cdif (f2,h)) . (n + 1)) . x)
proofend;

theorem :: DIFF_3:14
for n being Element of NAT
for r, h, x being Real
for f1, f2 being Function of REAL,REAL holds ((cdif ((f1 + (r (#) f2)),h)) . (n + 1)) . x = (((cdif (f1,h)) . (n + 1)) . x) + (r * (((cdif (f2,h)) . (n + 1)) . x))
proofend;

theorem :: DIFF_3:15
for n being Element of NAT
for r1, r2, h, x being Real
for f1, f2 being Function of REAL,REAL holds ((cdif (((r1 (#) f1) - (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((cdif (f1,h)) . (n + 1)) . x)) - (r2 * (((cdif (f2,h)) . (n + 1)) . x))
proofend;

theorem Th16: :: DIFF_3:16
for h being Real
for f being Function of REAL,REAL holds (cdif (f,h)) . 1 = cD (f,h)
proofend;

theorem :: DIFF_3:17
for m, n being Element of NAT
for h, x being Real
for f being Function of REAL,REAL holds ((cdif (((cdif (f,h)) . m),h)) . n) . x = ((cdif (f,h)) . (m + n)) . x
proofend;

theorem :: DIFF_3:18
for n being Element of NAT
for h, x being Real
for f being Function of REAL,REAL st ((fdif (f,h)) . n) . x = ((cdif (f,h)) . n) . (x + ((n / 2) * h)) holds
((bdif (f,h)) . n) . x = ((cdif (f,h)) . n) . (x - ((n / 2) * h))
proofend;

theorem :: DIFF_3:19
for n being Element of NAT
for h, x being Real
for f being Function of REAL,REAL st ((fdif (f,h)) . n) . x = ((cdif (f,h)) . n) . ((x + (((n - 1) / 2) * h)) + (h / 2)) holds
((bdif (f,h)) . n) . x = ((cdif (f,h)) . n) . ((x - (((n - 1) / 2) * h)) - (h / 2))
proofend;

theorem :: DIFF_3:20
for x, h being Real
for f being Function of REAL,REAL holds [!f,x,(x + h)!] = ((fD (f,h)) . x) / h
proofend;

theorem :: DIFF_3:21
for x, h being Real
for f being Function of REAL,REAL holds [!f,(x - h),x!] = ((bD (f,h)) . x) / h
proofend;

theorem Th22: :: DIFF_3:22
for x, h being Real
for f being Function of REAL,REAL holds [!f,(x - (h / 2)),(x + (h / 2))!] = ((cD (f,h)) . x) / h
proofend;

theorem Th23: :: DIFF_3:23
for x, h being Real
for f being Function of REAL,REAL holds [!f,(x - (h / 2)),(x + (h / 2))!] = (((cdif (f,h)) . 1) . x) / h
proofend;

theorem :: DIFF_3:24
for h, x being Real
for f being Function of REAL,REAL st h <> 0 holds
[!f,(x - h),x,(x + h)!] = (((cdif (f,h)) . 2) . x) / ((2 * h) * h)
proofend;

theorem Th25: :: DIFF_3:25
for x0, x1 being Real
for f1, f2 being Function of REAL,REAL holds [!(f1 - f2),x0,x1!] = [!f1,x0,x1!] - [!f2,x0,x1!]
proofend;

theorem :: DIFF_3:26
for r, x0, x1 being Real
for f1, f2 being Function of REAL,REAL holds [!((r (#) f1) + f2),x0,x1!] = (r * [!f1,x0,x1!]) + [!f2,x0,x1!]
proofend;

theorem :: DIFF_3:27
for r, x0, x1 being Real
for f1, f2 being Function of REAL,REAL holds [!((r (#) f1) - f2),x0,x1!] = (r * [!f1,x0,x1!]) - [!f2,x0,x1!]
proofend;

theorem :: DIFF_3:28
for r, x0, x1 being Real
for f1, f2 being Function of REAL,REAL holds [!(f1 + (r (#) f2)),x0,x1!] = [!f1,x0,x1!] + (r * [!f2,x0,x1!])
proofend;

theorem :: DIFF_3:29
for r, x0, x1 being Real
for f1, f2 being Function of REAL,REAL holds [!(f1 - (r (#) f2)),x0,x1!] = [!f1,x0,x1!] - (r * [!f2,x0,x1!])
proofend;

theorem :: DIFF_3:30
for r1, r2, x0, x1 being Real
for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) - (r2 (#) f2)),x0,x1!] = (r1 * [!f1,x0,x1!]) - (r2 * [!f2,x0,x1!])
proofend;

theorem Th31: :: DIFF_3:31
for h, x being Real
for f1, f2 being Function of REAL,REAL holds ((bdif ((f1 (#) f2),h)) . 1) . x = ((f1 . x) * (((bdif (f2,h)) . 1) . x)) + ((f2 . (x - h)) * (((bdif (f1,h)) . 1) . x))
proofend;

theorem :: DIFF_3:32
for x0, x1, x2 being Real
for f being Function of REAL,REAL st x0,x1,x2 are_mutually_different holds
[!f,x0,x1,x2!] = [!f,x0,x2,x1!]
proofend;

theorem :: DIFF_3:33
for h, x being Real
for f1, f2 being Function of REAL,REAL
for S being Seq_Sequence st ( for n, i being Nat st i <= n holds
(S . n) . i = ((n choose i) * (((bdif (f1,h)) . i) . x)) * (((bdif (f2,h)) . (n -' i)) . (x - (i * h))) ) holds
( ((bdif ((f1 (#) f2),h)) . 1) . x = Sum ((S . 1),1) &amp; ((bdif ((f1 (#) f2),h)) . 2) . x = Sum ((S . 2),2) )
proofend;

theorem Th34: :: DIFF_3:34
for h, x being Real
for f1, f2 being Function of REAL,REAL holds ((cdif ((f1 (#) f2),h)) . 1) . x = ((f1 . (x + (h / 2))) * (((cdif (f2,h)) . 1) . x)) + ((f2 . (x - (h / 2))) * (((cdif (f1,h)) . 1) . x))
proofend;

theorem :: DIFF_3:35
for h, x being Real
for f1, f2 being Function of REAL,REAL
for S being Seq_Sequence st ( for n, i being Nat st i <= n holds
(S . n) . i = ((n choose i) * (((cdif (f1,h)) . i) . (x + ((n -' i) * (h / 2))))) * (((cdif (f2,h)) . (n -' i)) . (x - (i * (h / 2)))) ) holds
( ((cdif ((f1 (#) f2),h)) . 1) . x = Sum ((S . 1),1) &amp; ((cdif ((f1 (#) f2),h)) . 2) . x = Sum ((S . 2),2) )
proofend;

:: f.x=sqrt x
theorem :: DIFF_3:36
for x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = sqrt x ) &amp; x0 <> x1 &amp; x0 > 0 &amp; x1 > 0 holds
[!f,x0,x1!] = 1 / ((sqrt x0) + (sqrt x1))
proofend;

theorem :: DIFF_3:37
for x0, x1, x2 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = sqrt x ) &amp; x0,x1,x2 are_mutually_different &amp; x0 > 0 &amp; x1 > 0 &amp; x2 > 0 holds
[!f,x0,x1,x2!] = - (1 / ((((sqrt x0) + (sqrt x1)) * ((sqrt x0) + (sqrt x2))) * ((sqrt x1) + (sqrt x2))))
proofend;

theorem :: DIFF_3:38
for x0, x1, x2, x3 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = sqrt x ) &amp; x0,x1,x2,x3 are_mutually_different &amp; x0 > 0 &amp; x1 > 0 &amp; x2 > 0 &amp; x3 > 0 holds
[!f,x0,x1,x2,x3!] = ((((sqrt x0) + (sqrt x1)) + (sqrt x2)) + (sqrt x3)) / (((((((sqrt x0) + (sqrt x1)) * ((sqrt x0) + (sqrt x2))) * ((sqrt x0) + (sqrt x3))) * ((sqrt x1) + (sqrt x2))) * ((sqrt x1) + (sqrt x3))) * ((sqrt x2) + (sqrt x3)))
proofend;

theorem :: DIFF_3:39
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = sqrt x ) &amp; x > 0 &amp; x + h > 0 holds
(fD (f,h)) . x = (sqrt (x + h)) - (sqrt x)
proofend;

theorem :: DIFF_3:40
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = sqrt x ) &amp; x > 0 &amp; x - h > 0 holds
(bD (f,h)) . x = (sqrt x) - (sqrt (x - h))
proofend;

theorem :: DIFF_3:41
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = sqrt x ) &amp; x + (h / 2) > 0 &amp; x - (h / 2) > 0 holds
(cD (f,h)) . x = (sqrt (x + (h / 2))) - (sqrt (x - (h / 2)))
proofend;

:: f.x=x^2
theorem :: DIFF_3:42
for x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = x ^2 ) &amp; x0 <> x1 holds
[!f,x0,x1!] = x0 + x1
proofend;

theorem :: DIFF_3:43
for x0, x1, x2 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = x ^2 ) &amp; x0,x1,x2 are_mutually_different holds
[!f,x0,x1,x2!] = 1
proofend;

theorem :: DIFF_3:44
for x0, x1, x2, x3 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = x ^2 ) &amp; x0,x1,x2,x3 are_mutually_different holds
[!f,x0,x1,x2,x3!] = 0
proofend;

theorem :: DIFF_3:45
for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = x ^2 ) holds
(fD (f,h)) . x = ((2 * x) * h) + (h ^2)
proofend;

theorem :: DIFF_3:46
for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = x ^2 ) holds
(bD (f,h)) . x = h * ((2 * x) - h)
proofend;

theorem :: DIFF_3:47
for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = x ^2 ) holds
(cD (f,h)) . x = (2 * h) * x
proofend;

:: f.x=k/(x^2)
theorem :: DIFF_3:48
for k, x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = k / (x ^2) ) &amp; x0 <> x1 &amp; x0 <> 0 &amp; x1 <> 0 holds
[!f,x0,x1!] = - ((k / (x0 * x1)) * ((1 / x0) + (1 / x1)))
proofend;

theorem :: DIFF_3:49
for k, x0, x1, x2 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = k / (x ^2) ) &amp; x0 <> 0 &amp; x1 <> 0 &amp; x2 <> 0 &amp; x0,x1,x2 are_mutually_different holds
[!f,x0,x1,x2!] = (k / ((x0 * x1) * x2)) * (((1 / x0) + (1 / x1)) + (1 / x2))
proofend;

theorem :: DIFF_3:50
for k, x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = k / (x ^2) ) &amp; x <> 0 &amp; x + h <> 0 holds
(fD (f,h)) . x = (((- k) * h) * ((2 * x) + h)) / (((x ^2) + (h * x)) ^2)
proofend;

theorem :: DIFF_3:51
for k, x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = k / (x ^2) ) &amp; x <> 0 &amp; x - h <> 0 holds
(bD (f,h)) . x = (((- k) * h) * ((2 * x) - h)) / (((x ^2) - (x * h)) ^2)
proofend;

theorem :: DIFF_3:52
for k, x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = k / (x ^2) ) &amp; x + (h / 2) <> 0 &amp; x - (h / 2) <> 0 holds
(cD (f,h)) . x = (- (((2 * h) * k) * x)) / (((x ^2) - ((h / 2) ^2)) ^2)
proofend;

:: f.x=(sin x)^3
theorem :: DIFF_3:53
for x0, x1 being Real holds [!((sin (#) sin) (#) sin),x0,x1!] = ((1 / 2) * (((3 * (cos ((x0 + x1) / 2))) * (sin ((x0 - x1) / 2))) - ((cos ((3 * (x0 + x1)) / 2)) * (sin ((3 * (x0 - x1)) / 2))))) / (x0 - x1)
proofend;

theorem :: DIFF_3:54
for h, x being Real holds (fD (((sin (#) sin) (#) sin),h)) . x = (1 / 2) * (((3 * (cos (((2 * x) + h) / 2))) * (sin (h / 2))) - ((cos ((3 * ((2 * x) + h)) / 2)) * (sin ((3 * h) / 2))))
proofend;

theorem :: DIFF_3:55
for h, x being Real holds (bD (((sin (#) sin) (#) sin),h)) . x = (1 / 2) * (((3 * (cos (((2 * x) - h) / 2))) * (sin (h / 2))) - ((cos ((3 * ((2 * x) - h)) / 2)) * (sin ((3 * h) / 2))))
proofend;

theorem :: DIFF_3:56
for h, x being Real holds (cD (((sin (#) sin) (#) sin),h)) . x = (1 / 2) * (((3 * (cos x)) * (sin (h / 2))) - ((cos (3 * x)) * (sin ((3 * h) / 2))))
proofend;

:: f.x=(cos x)^3
theorem :: DIFF_3:57
for x0, x1 being Real holds [!((cos (#) cos) (#) cos),x0,x1!] = - (((1 / 2) * (((3 * (sin ((x0 + x1) / 2))) * (sin ((x0 - x1) / 2))) + ((sin (((3 * x0) + (3 * x1)) / 2)) * (sin (((3 * x0) - (3 * x1)) / 2))))) / (x0 - x1))
proofend;

theorem :: DIFF_3:58
for h, x being Real holds (fD (((cos (#) cos) (#) cos),h)) . x = - ((1 / 2) * (((3 * (sin (((2 * x) + h) / 2))) * (sin (h / 2))) + ((sin ((3 * ((2 * x) + h)) / 2)) * (sin ((3 * h) / 2)))))
proofend;

theorem :: DIFF_3:59
for h, x being Real holds (bD (((cos (#) cos) (#) cos),h)) . x = - ((1 / 2) * (((3 * (sin (((2 * x) - h) / 2))) * (sin (h / 2))) + ((sin ((3 * ((2 * x) - h)) / 2)) * (sin ((3 * h) / 2)))))
proofend;

theorem :: DIFF_3:60
for h, x being Real holds (cD (((cos (#) cos) (#) cos),h)) . x = - ((1 / 2) * (((3 * (sin x)) * (sin (h / 2))) + ((sin (3 * x)) * (sin ((3 * h) / 2)))))
proofend;

:: f.x=1/sin(x)
theorem :: DIFF_3:61
for x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / (sin x) ) &amp; sin x0 <> 0 &amp; sin x1 <> 0 holds
[!f,x0,x1!] = - (((2 * ((sin x1) - (sin x0))) / ((cos (x0 + x1)) - (cos (x0 - x1)))) / (x0 - x1))
proofend;

theorem :: DIFF_3:62
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / (sin x) ) &amp; sin x <> 0 &amp; sin (x + h) <> 0 holds
(fD (f,h)) . x = - ((2 * ((sin x) - (sin (x + h)))) / ((cos ((2 * x) + h)) - (cos h)))
proofend;

theorem :: DIFF_3:63
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / (sin x) ) &amp; sin x <> 0 &amp; sin (x - h) <> 0 holds
(bD (f,h)) . x = ((- 2) * ((sin (x - h)) - (sin x))) / ((cos ((2 * x) - h)) - (cos h))
proofend;

theorem :: DIFF_3:64
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / (sin x) ) &amp; sin (x + (h / 2)) <> 0 &amp; sin (x - (h / 2)) <> 0 holds
(cD (f,h)) . x = - ((2 * ((sin (x - (h / 2))) - (sin (x + (h / 2))))) / ((cos (2 * x)) - (cos h)))
proofend;

:: f.x=1/cos(x)
theorem :: DIFF_3:65
for x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / (cos x) ) &amp; x0 <> x1 &amp; cos x0 <> 0 &amp; cos x1 <> 0 holds
[!f,x0,x1!] = ((2 * ((cos x1) - (cos x0))) / ((cos (x0 + x1)) + (cos (x0 - x1)))) / (x0 - x1)
proofend;

theorem :: DIFF_3:66
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / (cos x) ) &amp; cos x <> 0 &amp; cos (x + h) <> 0 holds
(fD (f,h)) . x = (2 * ((cos x) - (cos (x + h)))) / ((cos ((2 * x) + h)) + (cos h))
proofend;

theorem :: DIFF_3:67
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / (cos x) ) &amp; cos x <> 0 &amp; cos (x - h) <> 0 holds
(bD (f,h)) . x = (2 * ((cos (x - h)) - (cos x))) / ((cos ((2 * x) - h)) + (cos h))
proofend;

theorem :: DIFF_3:68
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / (cos x) ) &amp; cos (x + (h / 2)) <> 0 &amp; cos (x - (h / 2)) <> 0 holds
(cD (f,h)) . x = (2 * ((cos (x - (h / 2))) - (cos (x + (h / 2))))) / ((cos (2 * x)) + (cos h))
proofend;

:: f.x=1/(sin(x))^2
theorem :: DIFF_3:69
for x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / ((sin x) ^2) ) &amp; x0 <> x1 &amp; sin x0 <> 0 &amp; sin x1 <> 0 holds
[!f,x0,x1!] = ((((16 * (cos ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) * (cos ((x1 - x0) / 2))) * (sin ((x1 + x0) / 2))) / ((((cos (x0 + x1)) - (cos (x0 - x1))) ^2) * (x0 - x1))
proofend;

theorem :: DIFF_3:70
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / ((sin x) ^2) ) &amp; sin x <> 0 &amp; sin (x + h) <> 0 holds
(fD (f,h)) . x = ((((16 * (cos (((2 * x) + h) / 2))) * (sin ((- h) / 2))) * (cos ((- h) / 2))) * (sin (((2 * x) + h) / 2))) / (((cos ((2 * x) + h)) - (cos h)) ^2)
proofend;

theorem :: DIFF_3:71
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / ((sin x) ^2) ) &amp; sin x <> 0 &amp; sin (x - h) <> 0 holds
(bD (f,h)) . x = ((((16 * (cos (((2 * x) - h) / 2))) * (sin ((- h) / 2))) * (cos ((- h) / 2))) * (sin (((2 * x) - h) / 2))) / (((cos ((2 * x) - h)) - (cos h)) ^2)
proofend;

theorem :: DIFF_3:72
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / ((sin x) ^2) ) &amp; sin (x + (h / 2)) <> 0 &amp; sin (x - (h / 2)) <> 0 holds
(cD (f,h)) . x = ((((16 * (cos x)) * (sin ((- h) / 2))) * (cos ((- h) / 2))) * (sin x)) / (((cos (2 * x)) - (cos h)) ^2)
proofend;

:: f.x=1/(cos(x)^2)
theorem :: DIFF_3:73
for x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / ((cos x) ^2) ) &amp; x0 <> x1 &amp; cos x0 <> 0 &amp; cos x1 <> 0 holds
[!f,x0,x1!] = ((((((- 16) * (sin ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) * (cos ((x1 + x0) / 2))) * (cos ((x1 - x0) / 2))) / (((cos (x0 + x1)) + (cos (x0 - x1))) ^2)) / (x0 - x1)
proofend;

theorem :: DIFF_3:74
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / ((cos x) ^2) ) &amp; cos x <> 0 &amp; cos (x + h) <> 0 holds
(fD (f,h)) . x = (((((- 16) * (sin (((2 * x) + h) / 2))) * (sin ((- h) / 2))) * (cos (((2 * x) + h) / 2))) * (cos ((- h) / 2))) / (((cos ((2 * x) + h)) + (cos h)) ^2)
proofend;

theorem :: DIFF_3:75
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / ((cos x) ^2) ) &amp; cos x <> 0 &amp; cos (x - h) <> 0 holds
(bD (f,h)) . x = (((((- 16) * (sin (((2 * x) - h) / 2))) * (sin ((- h) / 2))) * (cos (((2 * x) - h) / 2))) * (cos ((- h) / 2))) / (((cos ((2 * x) - h)) + (cos h)) ^2)
proofend;

theorem :: DIFF_3:76
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / ((cos x) ^2) ) &amp; cos (x + (h / 2)) <> 0 &amp; cos (x - (h / 2)) <> 0 holds
(cD (f,h)) . x = (((((- 16) * (sin x)) * (sin ((- h) / 2))) * (cos x)) * (cos ((- h) / 2))) / (((cos (2 * x)) + (cos h)) ^2)
proofend;

:: f.x=tan(x)*sin(x)
theorem :: DIFF_3:77
for x0, x1 being Real st x0 in dom tan &amp; x1 in dom tan holds
[!(tan (#) sin),x0,x1!] = ((((1 / (cos x0)) - (cos x0)) - (1 / (cos x1))) + (cos x1)) / (x0 - x1)
proofend;

theorem :: DIFF_3:78
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (tan (#) sin) . x ) &amp; x in dom tan &amp; x + h in dom tan holds
(fD (f,h)) . x = (((1 / (cos (x + h))) - (cos (x + h))) - (1 / (cos x))) + (cos x)
proofend;

theorem :: DIFF_3:79
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (tan (#) sin) . x ) &amp; x in dom tan &amp; x - h in dom tan holds
(bD (f,h)) . x = (((1 / (cos x)) - (cos x)) - (1 / (cos (x - h)))) + (cos (x - h))
proofend;

theorem :: DIFF_3:80
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (tan (#) sin) . x ) &amp; x + (h / 2) in dom tan &amp; x - (h / 2) in dom tan holds
(cD (f,h)) . x = (((1 / (cos (x + (h / 2)))) - (cos (x + (h / 2)))) - (1 / (cos (x - (h / 2))))) + (cos (x - (h / 2)))
proofend;

:: f.x=tan(x)*cos(x)
theorem :: DIFF_3:81
for x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (tan (#) cos) . x ) &amp; x0 in dom tan &amp; x1 in dom tan holds
[!f,x0,x1!] = ((sin x0) - (sin x1)) / (x0 - x1)
proofend;

theorem :: DIFF_3:82
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (tan (#) cos) . x ) &amp; x in dom tan &amp; x + h in dom tan holds
(fD (f,h)) . x = (sin (x + h)) - (sin x)
proofend;

theorem :: DIFF_3:83
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (tan (#) cos) . x ) &amp; x in dom tan &amp; x - h in dom tan holds
(bD (f,h)) . x = (sin x) - (sin (x - h))
proofend;

theorem :: DIFF_3:84
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (tan (#) cos) . x ) &amp; x + (h / 2) in dom tan &amp; x - (h / 2) in dom tan holds
(cD (f,h)) . x = (sin (x + (h / 2))) - (sin (x - (h / 2)))
proofend;

:: f.x=cot(x)*cos(x)
theorem :: DIFF_3:85
for x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (cot (#) cos) . x ) &amp; x0 in dom cot &amp; x1 in dom cot holds
[!f,x0,x1!] = ((((1 / (sin x0)) - (sin x0)) - (1 / (sin x1))) + (sin x1)) / (x0 - x1)
proofend;

theorem :: DIFF_3:86
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (cot (#) cos) . x ) &amp; x in dom cot &amp; x + h in dom cot holds
(fD (f,h)) . x = (((1 / (sin (x + h))) - (sin (x + h))) - (1 / (sin x))) + (sin x)
proofend;

theorem :: DIFF_3:87
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (cot (#) cos) . x ) &amp; x in dom cot &amp; x - h in dom cot holds
(bD (f,h)) . x = (((1 / (sin x)) - (sin x)) - (1 / (sin (x - h)))) + (sin (x - h))
proofend;

theorem :: DIFF_3:88
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (cot (#) cos) . x ) &amp; x + (h / 2) in dom cot &amp; x - (h / 2) in dom cot holds
(cD (f,h)) . x = (((1 / (sin (x + (h / 2)))) - (sin (x + (h / 2)))) - (1 / (sin (x - (h / 2))))) + (sin (x - (h / 2)))
proofend;

:: f.x=cot(x)*sin(x)
theorem :: DIFF_3:89
for x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (cot (#) sin) . x ) &amp; x0 in dom cot &amp; x1 in dom cot holds
[!f,x0,x1!] = ((cos x0) - (cos x1)) / (x0 - x1)
proofend;

theorem :: DIFF_3:90
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (cot (#) sin) . x ) &amp; x in dom cot &amp; x + h in dom cot holds
(fD (f,h)) . x = (cos (x + h)) - (cos x)
proofend;

theorem :: DIFF_3:91
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (cot (#) sin) . x ) &amp; x in dom cot &amp; x - h in dom cot holds
(bD (f,h)) . x = (cos x) - (cos (x - h))
proofend;

theorem :: DIFF_3:92
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (cot (#) sin) . x ) &amp; x + (h / 2) in dom cot &amp; x - (h / 2) in dom cot holds
(cD (f,h)) . x = (cos (x + (h / 2))) - (cos (x - (h / 2)))
proofend;

:: f.x=(tan(x))^2
theorem :: DIFF_3:93
for x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (tan (#) tan) . x ) &amp; x0 in dom tan &amp; x1 in dom tan holds
[!f,x0,x1!] = (((cos x1) ^2) - ((cos x0) ^2)) / ((((cos x0) * (cos x1)) ^2) * (x0 - x1))
proofend;

theorem :: DIFF_3:94
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (tan (#) tan) . x ) &amp; x in dom tan &amp; x + h in dom tan holds
(fD (f,h)) . x = - (((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) / (((cos (x + h)) * (cos x)) ^2))
proofend;

theorem :: DIFF_3:95
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (tan (#) tan) . x ) &amp; x in dom tan &amp; x - h in dom tan holds
(bD (f,h)) . x = - (((1 / 2) * ((cos (2 * x)) - (cos (2 * (h - x))))) / (((cos x) * (cos (x - h))) ^2))
proofend;

theorem :: DIFF_3:96
for x, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (tan (#) tan) . x ) &amp; x + (h / 2) in dom tan &amp; x - (h / 2) in dom tan holds
(cD (f,h)) . x = - (((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x))))) / (((cos (x + (h / 2))) * (cos (x - (h / 2)))) ^2))
proofend;