:: DIFF_4 semantic presentation

begin


theorem Th1: :: DIFF_4:1
for x0, x1 being Real st x0 > 0 & x1 > 0 holds
(log (number_e,x0)) - (log (number_e,x1)) = log (number_e,(x0 / x1))
proof
let x0, x1 be Real; ::_thesis: ( x0 > 0 & x1 > 0 implies (log (number_e,x0)) - (log (number_e,x1)) = log (number_e,(x0 / x1)) )
assume A1: ( x0 > 0 & x1 > 0 ) ; ::_thesis: (log (number_e,x0)) - (log (number_e,x1)) = log (number_e,(x0 / x1))
 number_e > 1 by TAYLOR_1:11, XXREAL_0:2;
hence  (log (number_e,x0)) - (log (number_e,x1)) = log (number_e,(x0 / x1)) by A1, POWER:54; ::_thesis: verum
end;

theorem :: DIFF_4:2
for x0, x1 being Real st x0 > 0 & x1 > 0 holds
(log (number_e,x0)) + (log (number_e,x1)) = log (number_e,(x0 * x1))
proof
let x0, x1 be Real; ::_thesis: ( x0 > 0 & x1 > 0 implies (log (number_e,x0)) + (log (number_e,x1)) = log (number_e,(x0 * x1)) )
assume A1: ( x0 > 0 & x1 > 0 ) ; ::_thesis: (log (number_e,x0)) + (log (number_e,x1)) = log (number_e,(x0 * x1))
 number_e > 1 by TAYLOR_1:11, XXREAL_0:2;
hence  (log (number_e,x0)) + (log (number_e,x1)) = log (number_e,(x0 * x1)) by A1, POWER:53; ::_thesis: verum
end;

theorem Th3: :: DIFF_4:3
for x being Real st x > 0 holds
log (number_e,x) = ln . x
proof
let x be Real; ::_thesis: ( x > 0 implies log (number_e,x) = ln . x )
assume A1: x > 0 ; ::_thesis: log (number_e,x) = ln . x
 x in right_open_halfline 0
proof
 x in  {  g where g is Real : 0 < g  }  by A1;
hence  x in right_open_halfline 0 by XXREAL_1:230; ::_thesis: verum
end;
hence  log (number_e,x) = ln . x by TAYLOR_1:def_2; ::_thesis: verum
end;

theorem Th4: :: DIFF_4:4
for x0, x1 being Real st x0 > 0 & x1 > 0 holds
(ln . x0) - (ln . x1) = ln . (x0 / x1)
proof
let x0, x1 be Real; ::_thesis: ( x0 > 0 & x1 > 0 implies (ln . x0) - (ln . x1) = ln . (x0 / x1) )
assume A1: ( x0 > 0 & x1 > 0 ) ; ::_thesis: (ln . x0) - (ln . x1) = ln . (x0 / x1)
A2: log (number_e,(x0 / x1)) = ln . (x0 / x1)
proof
A3: x0 / x1 in REAL by XREAL_0:def_1;
 x0 / x1 in right_open_halfline 0
proof
 x0 / x1 in  {  g where g is Real : 0 < g  }  by A1, A3;
hence  x0 / x1 in right_open_halfline 0 by XXREAL_1:230; ::_thesis: verum
end;
hence  log (number_e,(x0 / x1)) = ln . (x0 / x1) by TAYLOR_1:def_2; ::_thesis: verum
end;
(ln . x0) - (ln . x1) = (log (number_e,x0)) - (ln . x1) by A1, Th3
.= (log (number_e,x0)) - (log (number_e,x1)) by A1, Th3
.= log (number_e,(x0 / x1)) by A1, Th1 ;
hence  (ln . x0) - (ln . x1) = ln . (x0 / x1) by A2; ::_thesis: verum
end;

theorem :: DIFF_4:5
for k, x0, x1, x2, x3 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = k / (x ^2) ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 & x0,x1,x2,x3 are_mutually_different holds
[!f,x0,x1,x2,x3!] = (k * (((1 / ((x1 * x2) * x0)) * (((1 / x0) + (1 / x2)) + (1 / x1))) - ((1 / ((x2 * x1) * x3)) * (((1 / x3) + (1 / x1)) + (1 / x2))))) / (x0 - x3)
proof
let k, x0, x1, x2, x3 be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = k / (x ^2) ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 & x0,x1,x2,x3 are_mutually_different holds
[!f,x0,x1,x2,x3!] = (k * (((1 / ((x1 * x2) * x0)) * (((1 / x0) + (1 / x2)) + (1 / x1))) - ((1 / ((x2 * x1) * x3)) * (((1 / x3) + (1 / x1)) + (1 / x2))))) / (x0 - x3)
let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = k / (x ^2) ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 & x0,x1,x2,x3 are_mutually_different implies [!f,x0,x1,x2,x3!] = (k * (((1 / ((x1 * x2) * x0)) * (((1 / x0) + (1 / x2)) + (1 / x1))) - ((1 / ((x2 * x1) * x3)) * (((1 / x3) + (1 / x1)) + (1 / x2))))) / (x0 - x3) )
assume that
A1: for x being Real holds f . x = k / (x ^2) and
A2: ( x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 ) and
A3: x0,x1,x2,x3 are_mutually_different ; ::_thesis: [!f,x0,x1,x2,x3!] = (k * (((1 / ((x1 * x2) * x0)) * (((1 / x0) + (1 / x2)) + (1 / x1))) - ((1 / ((x2 * x1) * x3)) * (((1 / x3) + (1 / x1)) + (1 / x2))))) / (x0 - x3)
 ( x0 <> x1 & x0 <> x2 & x1 <> x2 ) by A3, ZFMISC_1:def_6;
then  x0,x1,x2 are_mutually_different by ZFMISC_1:def_5;
then A4: [!f,x0,x1,x2!] = (k / ((x0 * x1) * x2)) * (((1 / x0) + (1 / x1)) + (1 / x2)) by A1, A2, DIFF_3:49
.= (k * (1 / ((x1 * x2) * x0))) * (((1 / x0) + (1 / x2)) + (1 / x1)) ;
 ( x1 <> x2 & x1 <> x3 & x2 <> x3 ) by A3, ZFMISC_1:def_6;
then  x1,x2,x3 are_mutually_different by ZFMISC_1:def_5;
then  [!f,x1,x2,x3!] = (k / ((x1 * x2) * x3)) * (((1 / x1) + (1 / x2)) + (1 / x3)) by A1, A2, DIFF_3:49;
hence  [!f,x0,x1,x2,x3!] = (k * (((1 / ((x1 * x2) * x0)) * (((1 / x0) + (1 / x2)) + (1 / x1))) - ((1 / ((x2 * x1) * x3)) * (((1 / x3) + (1 / x1)) + (1 / x2))))) / (x0 - x3) by A4; ::_thesis: verum
end;

theorem :: DIFF_4:6
for x0, x1 being Real st x0 in dom cot & x1 in dom cot holds
[!(cot (#) cot),x0,x1!] = - ((((cos x1) ^2) - ((cos x0) ^2)) / ((((sin x0) * (sin x1)) ^2) * (x0 - x1)))
proof
let x0, x1 be Real; ::_thesis: ( x0 in dom cot & x1 in dom cot implies [!(cot (#) cot),x0,x1!] = - ((((cos x1) ^2) - ((cos x0) ^2)) / ((((sin x0) * (sin x1)) ^2) * (x0 - x1))) )
assume A1: ( x0 in dom cot & x1 in dom cot ) ; ::_thesis: [!(cot (#) cot),x0,x1!] = - ((((cos x1) ^2) - ((cos x0) ^2)) / ((((sin x0) * (sin x1)) ^2) * (x0 - x1)))
A2: ( sin x0 <> 0 & sin x1 <> 0 ) by A1, FDIFF_8:2;
[!(cot (#) cot),x0,x1!] = (((cot . x0) * (cot . x0)) - ((cot (#) cot) . x1)) / (x0 - x1) by VALUED_1:5
.= (((cot . x0) * (cot . x0)) - ((cot . x1) * (cot . x1))) / (x0 - x1) by VALUED_1:5
.= ((((cos . x0) * ((sin . x0) ")) * (cot . x0)) - ((cot . x1) * (cot . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1
.= ((((cos . x0) * ((sin . x0) ")) * ((cos . x0) * ((sin . x0) "))) - ((cot . x1) * (cot . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1
.= ((((cos . x0) * ((sin . x0) ")) * ((cos . x0) * ((sin . x0) "))) - (((cos . x1) * ((sin . x1) ")) * (cot . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1
.= (((cot x0) ^2) - ((cot x1) ^2)) / (x0 - x1) by A1, RFUNCT_1:def_1
.= (((cot x0) - (cot x1)) * ((cot x0) + (cot x1))) / (x0 - x1)
.= ((- ((sin (x0 - x1)) / ((sin x0) * (sin x1)))) * ((cot x0) + (cot x1))) / (x0 - x1) by A2, SIN_COS4:24
.= (- (((sin (x0 - x1)) / ((sin x0) * (sin x1))) * ((cot x0) + (cot x1)))) / (x0 - x1)
.= (- (((sin (x0 - x1)) / ((sin x0) * (sin x1))) * ((sin (x0 + x1)) / ((sin x0) * (sin x1))))) / (x0 - x1) by A2, SIN_COS4:23
.= (- (((sin (x0 + x1)) * (sin (x0 - x1))) / (((sin x0) * (sin x1)) ^2))) / (x0 - x1) by XCMPLX_1:76
.= (- ((((cos x1) ^2) - ((cos x0) ^2)) / (((sin x0) * (sin x1)) ^2))) / (x0 - x1) by SIN_COS4:38
.= - (((((cos x1) ^2) - ((cos x0) ^2)) / (((sin x0) * (sin x1)) ^2)) / (x0 - x1))
.= - ((((cos x1) ^2) - ((cos x0) ^2)) / ((((sin x0) * (sin x1)) ^2) * (x0 - x1))) by XCMPLX_1:78 ;
hence  [!(cot (#) cot),x0,x1!] = - ((((cos x1) ^2) - ((cos x0) ^2)) / ((((sin x0) * (sin x1)) ^2) * (x0 - x1))) ; ::_thesis: verum
end;

theorem :: DIFF_4:7
for x, h being Real st x in dom cot & x + h in dom cot holds
(fD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) / (((sin (x + h)) * (sin x)) ^2)
proof
let x, h be Real; ::_thesis: ( x in dom cot & x + h in dom cot implies (fD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) / (((sin (x + h)) * (sin x)) ^2) )
set f = cot (#) cot;
assume A1: ( x in dom cot & x + h in dom cot ) ; ::_thesis: (fD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) / (((sin (x + h)) * (sin x)) ^2)
A2: ( sin x <> 0 & sin (x + h) <> 0 ) by A1, FDIFF_8:2;
 ( x in dom (cot (#) cot) & x + h in dom (cot (#) cot) )
proof
 ( x in (dom cot) /\ (dom cot) & x + h in (dom cot) /\ (dom cot) ) by A1;
hence  ( x in dom (cot (#) cot) & x + h in dom (cot (#) cot) ) by VALUED_1:def_4; ::_thesis: verum
end;
then (fD ((cot (#) cot),h)) . x = ((cot (#) cot) . (x + h)) - ((cot (#) cot) . x) by DIFF_1:1
.= ((cot . (x + h)) * (cot . (x + h))) - ((cot (#) cot) . x) by VALUED_1:5
.= ((cot . (x + h)) * (cot . (x + h))) - ((cot . x) * (cot . x)) by VALUED_1:5
.= (((cos . (x + h)) * ((sin . (x + h)) ")) * (cot . (x + h))) - ((cot . x) * (cot . x)) by A1, RFUNCT_1:def_1
.= (((cos . (x + h)) * ((sin . (x + h)) ")) * ((cos . (x + h)) * ((sin . (x + h)) "))) - ((cot . x) * (cot . x)) by A1, RFUNCT_1:def_1
.= (((cos . (x + h)) * ((sin . (x + h)) ")) * ((cos . (x + h)) * ((sin . (x + h)) "))) - (((cos . x) * ((sin . x) ")) * (cot . x)) by A1, RFUNCT_1:def_1
.= ((cot (x + h)) ^2) - ((cot x) ^2) by A1, RFUNCT_1:def_1
.= ((cot (x + h)) - (cot x)) * ((cot (x + h)) + (cot x))
.= (- ((sin ((x + h) - x)) / ((sin (x + h)) * (sin x)))) * ((cot (x + h)) + (cot x)) by A2, SIN_COS4:24
.= (- ((sin ((x + h) - x)) / ((sin (x + h)) * (sin x)))) * ((sin ((x + h) + x)) / ((sin (x + h)) * (sin x))) by A2, SIN_COS4:23
.= - (((sin ((x + h) - x)) / ((sin (x + h)) * (sin x))) * ((sin ((x + h) + x)) / ((sin (x + h)) * (sin x))))
.= - (((sin ((2 * x) + h)) * (sin h)) / (((sin (x + h)) * (sin x)) ^2)) by XCMPLX_1:76
.= - ((- ((1 / 2) * ((cos (((2 * x) + h) + h)) - (cos (((2 * x) + h) - h))))) / (((sin (x + h)) * (sin x)) ^2)) by SIN_COS4:29
.= ((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) / (((sin (x + h)) * (sin x)) ^2) ;
hence  (fD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) / (((sin (x + h)) * (sin x)) ^2) ; ::_thesis: verum
end;

theorem :: DIFF_4:8
for x, h being Real st x in dom cot & x - h in dom cot holds
(bD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (2 * x)) - (cos (2 * (h - x))))) / (((sin x) * (sin (x - h))) ^2)
proof
let x, h be Real; ::_thesis: ( x in dom cot & x - h in dom cot implies (bD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (2 * x)) - (cos (2 * (h - x))))) / (((sin x) * (sin (x - h))) ^2) )
set f = cot (#) cot;
assume A1: ( x in dom cot & x - h in dom cot ) ; ::_thesis: (bD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (2 * x)) - (cos (2 * (h - x))))) / (((sin x) * (sin (x - h))) ^2)
A2: ( sin x <> 0 & sin (x - h) <> 0 ) by A1, FDIFF_8:2;
 ( x in dom (cot (#) cot) & x - h in dom (cot (#) cot) )
proof
 ( x in (dom cot) /\ (dom cot) & x - h in (dom cot) /\ (dom cot) ) by A1;
hence  ( x in dom (cot (#) cot) & x - h in dom (cot (#) cot) ) by VALUED_1:def_4; ::_thesis: verum
end;
then (bD ((cot (#) cot),h)) . x = ((cot (#) cot) . x) - ((cot (#) cot) . (x - h)) by DIFF_1:38
.= ((cot . x) * (cot . x)) - ((cot (#) cot) . (x - h)) by VALUED_1:5
.= ((cot . x) * (cot . x)) - ((cot . (x - h)) * (cot . (x - h))) by VALUED_1:5
.= (((cos . x) * ((sin . x) ")) * (cot . x)) - ((cot . (x - h)) * (cot . (x - h))) by A1, RFUNCT_1:def_1
.= (((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) - ((cot . (x - h)) * (cot . (x - h))) by A1, RFUNCT_1:def_1
.= (((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) - (((cos . (x - h)) * ((sin . (x - h)) ")) * (cot . (x - h))) by A1, RFUNCT_1:def_1
.= ((cot x) ^2) - ((cot (x - h)) ^2) by A1, RFUNCT_1:def_1
.= ((cot x) - (cot (x - h))) * ((cot x) + (cot (x - h)))
.= (- ((sin (x - (x - h))) / ((sin x) * (sin (x - h))))) * ((cot x) + (cot (x - h))) by A2, SIN_COS4:24
.= - (((sin (x - (x - h))) / ((sin x) * (sin (x - h)))) * ((cot x) + (cot (x - h))))
.= - (((sin h) / ((sin x) * (sin (x - h)))) * ((sin (x + (x - h))) / ((sin x) * (sin (x - h))))) by A2, SIN_COS4:23
.= - (((sin h) * (sin ((2 * x) - h))) / (((sin x) * (sin (x - h))) ^2)) by XCMPLX_1:76
.= - ((- ((1 / 2) * ((cos (h + ((2 * x) - h))) - (cos (h - ((2 * x) - h)))))) / (((sin x) * (sin (x - h))) ^2)) by SIN_COS4:29
.= ((1 / 2) * ((cos (2 * x)) - (cos (2 * (h - x))))) / (((sin x) * (sin (x - h))) ^2) ;
hence  (bD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (2 * x)) - (cos (2 * (h - x))))) / (((sin x) * (sin (x - h))) ^2) ; ::_thesis: verum
end;

theorem :: DIFF_4:9
for x, h being Real st x + (h / 2) in dom cot & x - (h / 2) in dom cot holds
(cD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x))))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2)
proof
let x, h be Real; ::_thesis: ( x + (h / 2) in dom cot & x - (h / 2) in dom cot implies (cD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x))))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2) )
set f = cot (#) cot;
assume A1: ( x + (h / 2) in dom cot & x - (h / 2) in dom cot ) ; ::_thesis: (cD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x))))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2)
A2: ( sin (x + (h / 2)) <> 0 & sin (x - (h / 2)) <> 0 ) by A1, FDIFF_8:2;
 ( x + (h / 2) in dom (cot (#) cot) & x - (h / 2) in dom (cot (#) cot) )
proof
 ( x + (h / 2) in (dom cot) /\ (dom cot) & x - (h / 2) in (dom cot) /\ (dom cot) ) by A1;
hence  ( x + (h / 2) in dom (cot (#) cot) & x - (h / 2) in dom (cot (#) cot) ) by VALUED_1:def_4; ::_thesis: verum
end;
then (cD ((cot (#) cot),h)) . x = ((cot (#) cot) . (x + (h / 2))) - ((cot (#) cot) . (x - (h / 2))) by DIFF_1:39
.= ((cot . (x + (h / 2))) * (cot . (x + (h / 2)))) - ((cot (#) cot) . (x - (h / 2))) by VALUED_1:5
.= ((cot . (x + (h / 2))) * (cot . (x + (h / 2)))) - ((cot . (x - (h / 2))) * (cot . (x - (h / 2)))) by VALUED_1:5
.= (((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * (cot . (x + (h / 2)))) - ((cot . (x - (h / 2))) * (cot . (x - (h / 2)))) by A1, RFUNCT_1:def_1
.= (((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * ((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) "))) - ((cot . (x - (h / 2))) * (cot . (x - (h / 2)))) by A1, RFUNCT_1:def_1
.= (((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * ((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) "))) - (((cos . (x - (h / 2))) * ((sin . (x - (h / 2))) ")) * (cot . (x - (h / 2)))) by A1, RFUNCT_1:def_1
.= ((cot (x + (h / 2))) ^2) - ((cot (x - (h / 2))) ^2) by A1, RFUNCT_1:def_1
.= ((cot (x + (h / 2))) - (cot (x - (h / 2)))) * ((cot (x + (h / 2))) + (cot (x - (h / 2))))
.= (- ((sin ((x + (h / 2)) - (x - (h / 2)))) / ((sin (x + (h / 2))) * (sin (x - (h / 2)))))) * ((cot (x + (h / 2))) + (cot (x - (h / 2)))) by A2, SIN_COS4:24
.= (- ((sin h) / ((sin (x + (h / 2))) * (sin (x - (h / 2)))))) * ((sin ((x + (h / 2)) + (x - (h / 2)))) / ((sin (x + (h / 2))) * (sin (x - (h / 2))))) by A2, SIN_COS4:23
.= - (((sin h) / ((sin (x + (h / 2))) * (sin (x - (h / 2))))) * ((sin ((x + (h / 2)) + (x - (h / 2)))) / ((sin (x + (h / 2))) * (sin (x - (h / 2))))))
.= - (((sin h) * (sin (2 * x))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2)) by XCMPLX_1:76
.= - ((- ((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x)))))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2)) by SIN_COS4:29
.= ((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x))))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2) ;
hence  (cD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x))))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2) ; ::_thesis: verum
end;

theorem :: DIFF_4:10
for x0, x1 being Real st x0 in dom cosec & x1 in dom cosec holds
[!(cosec (#) cosec),x0,x1!] = (4 * ((sin (x1 + x0)) * (sin (x1 - x0)))) / ((((cos (x0 + x1)) - (cos (x0 - x1))) ^2) * (x0 - x1))
proof
let x0, x1 be Real; ::_thesis: ( x0 in dom cosec & x1 in dom cosec implies [!(cosec (#) cosec),x0,x1!] = (4 * ((sin (x1 + x0)) * (sin (x1 - x0)))) / ((((cos (x0 + x1)) - (cos (x0 - x1))) ^2) * (x0 - x1)) )
assume A1: ( x0 in dom cosec & x1 in dom cosec ) ; ::_thesis: [!(cosec (#) cosec),x0,x1!] = (4 * ((sin (x1 + x0)) * (sin (x1 - x0)))) / ((((cos (x0 + x1)) - (cos (x0 - x1))) ^2) * (x0 - x1))
A2: ( sin . x0 <> 0 & sin . x1 <> 0 ) by A1, RFUNCT_1:3;
[!(cosec (#) cosec),x0,x1!] = (((cosec . x0) * (cosec . x0)) - ((cosec (#) cosec) . x1)) / (x0 - x1) by VALUED_1:5
.= (((cosec . x0) * (cosec . x0)) - ((cosec . x1) * (cosec . x1))) / (x0 - x1) by VALUED_1:5
.= ((((sin . x0) ") * (cosec . x0)) - ((cosec . x1) * (cosec . x1))) / (x0 - x1) by A1, RFUNCT_1:def_2
.= ((((sin . x0) ") * ((sin . x0) ")) - ((cosec . x1) * (cosec . x1))) / (x0 - x1) by A1, RFUNCT_1:def_2
.= ((((sin . x0) ") * ((sin . x0) ")) - (((sin . x1) ") * (cosec . x1))) / (x0 - x1) by A1, RFUNCT_1:def_2
.= ((((sin . x0) ") ^2) - (((sin . x1) ") ^2)) / (x0 - x1) by A1, RFUNCT_1:def_2
.= (((1 / (sin . x0)) - (1 / (sin . x1))) * ((1 / (sin . x0)) + (1 / (sin . x1)))) / (x0 - x1)
.= ((((1 * (sin . x1)) - (1 * (sin . x0))) / ((sin . x0) * (sin . x1))) * ((1 / (sin . x0)) + (1 / (sin . x1)))) / (x0 - x1) by A2, XCMPLX_1:130
.= ((((sin . x1) - (sin . x0)) / ((sin . x0) * (sin . x1))) * (((sin . x1) + (sin . x0)) / ((sin . x0) * (sin . x1)))) / (x0 - x1) by A2, XCMPLX_1:116
.= ((((sin . x1) - (sin . x0)) * ((sin . x1) + (sin . x0))) / (((sin . x0) * (sin . x1)) * ((sin . x0) * (sin . x1)))) / (x0 - x1) by XCMPLX_1:76
.= ((((sin x1) * (sin x1)) - ((sin x0) * (sin x0))) / (((sin x0) * (sin x1)) ^2)) / (x0 - x1)
.= (((sin (x1 + x0)) * (sin (x1 - x0))) / (((sin x0) * (sin x1)) ^2)) / (x0 - x1) by SIN_COS4:37
.= (((sin (x1 + x0)) * (sin (x1 - x0))) / ((- ((1 / 2) * ((cos (x0 + x1)) - (cos (x0 - x1))))) ^2)) / (x0 - x1) by SIN_COS4:29
.= ((1 * ((sin (x1 + x0)) * (sin (x1 - x0)))) / ((1 / 4) * (((cos (x0 + x1)) - (cos (x0 - x1))) ^2))) / (x0 - x1)
.= ((1 / (1 / 4)) * (((sin (x1 + x0)) * (sin (x1 - x0))) / (((cos (x0 + x1)) - (cos (x0 - x1))) ^2))) / (x0 - x1) by XCMPLX_1:76
.= ((4 * ((sin (x1 + x0)) * (sin (x1 - x0)))) / (((cos (x0 + x1)) - (cos (x0 - x1))) ^2)) / (x0 - x1)
.= (4 * ((sin (x1 + x0)) * (sin (x1 - x0)))) / ((((cos (x0 + x1)) - (cos (x0 - x1))) ^2) * (x0 - x1)) by XCMPLX_1:78 ;
hence  [!(cosec (#) cosec),x0,x1!] = (4 * ((sin (x1 + x0)) * (sin (x1 - x0)))) / ((((cos (x0 + x1)) - (cos (x0 - x1))) ^2) * (x0 - x1)) ; ::_thesis: verum
end;

theorem :: DIFF_4:11
for x, h being Real st x in dom cosec & x + h in dom cosec holds
(fD ((cosec (#) cosec),h)) . x = - (((4 * (sin ((2 * x) + h))) * (sin h)) / (((cos ((2 * x) + h)) - (cos h)) ^2))
proof
let x, h be Real; ::_thesis: ( x in dom cosec & x + h in dom cosec implies (fD ((cosec (#) cosec),h)) . x = - (((4 * (sin ((2 * x) + h))) * (sin h)) / (((cos ((2 * x) + h)) - (cos h)) ^2)) )
set f = cosec (#) cosec;
assume A1: ( x in dom cosec & x + h in dom cosec ) ; ::_thesis: (fD ((cosec (#) cosec),h)) . x = - (((4 * (sin ((2 * x) + h))) * (sin h)) / (((cos ((2 * x) + h)) - (cos h)) ^2))
A2: ( sin . x <> 0 & sin . (x + h) <> 0 ) by A1, RFUNCT_1:3;
 ( x in dom (cosec (#) cosec) & x + h in dom (cosec (#) cosec) )
proof
 ( x in (dom cosec) /\ (dom cosec) & x + h in (dom cosec) /\ (dom cosec) ) by A1;
hence  ( x in dom (cosec (#) cosec) & x + h in dom (cosec (#) cosec) ) by VALUED_1:def_4; ::_thesis: verum
end;
then (fD ((cosec (#) cosec),h)) . x = ((cosec (#) cosec) . (x + h)) - ((cosec (#) cosec) . x) by DIFF_1:1
.= ((cosec . (x + h)) * (cosec . (x + h))) - ((cosec (#) cosec) . x) by VALUED_1:5
.= ((cosec . (x + h)) * (cosec . (x + h))) - ((cosec . x) * (cosec . x)) by VALUED_1:5
.= (((sin . (x + h)) ") * (cosec . (x + h))) - ((cosec . x) * (cosec . x)) by A1, RFUNCT_1:def_2
.= (((sin . (x + h)) ") * ((sin . (x + h)) ")) - ((cosec . x) * (cosec . x)) by A1, RFUNCT_1:def_2
.= (((sin . (x + h)) ") * ((sin . (x + h)) ")) - (((sin . x) ") * (cosec . x)) by A1, RFUNCT_1:def_2
.= (((sin . (x + h)) ") ^2) - (((sin . x) ") ^2) by A1, RFUNCT_1:def_2
.= ((1 / (sin . (x + h))) - (1 / (sin . x))) * ((1 / (sin . (x + h))) + (1 / (sin . x)))
.= (((1 * (sin . x)) - (1 * (sin . (x + h)))) / ((sin . (x + h)) * (sin . x))) * ((1 / (sin . (x + h))) + (1 / (sin . x))) by A2, XCMPLX_1:130
.= (((sin . x) - (sin . (x + h))) / ((sin . (x + h)) * (sin . x))) * (((sin . x) + (sin . (x + h))) / ((sin . (x + h)) * (sin . x))) by A2, XCMPLX_1:116
.= (((sin . x) - (sin . (x + h))) * ((sin . x) + (sin . (x + h)))) / (((sin . (x + h)) * (sin . x)) * ((sin . (x + h)) * (sin . x))) by XCMPLX_1:76
.= (((sin x) * (sin x)) - ((sin (x + h)) * (sin (x + h)))) / (((sin (x + h)) * (sin x)) ^2)
.= ((sin (x + (x + h))) * (sin (x - (x + h)))) / (((sin (x + h)) * (sin x)) ^2) by SIN_COS4:37
.= ((sin ((2 * x) + h)) * (sin (- h))) / ((- ((1 / 2) * ((cos ((x + h) + x)) - (cos ((x + h) - x))))) ^2) by SIN_COS4:29
.= ((sin ((2 * x) + h)) * (- (sin h))) / ((1 / 4) * (((cos ((2 * x) + h)) - (cos h)) ^2)) by SIN_COS:31
.= - ((1 * ((sin ((2 * x) + h)) * (sin h))) / ((1 / 4) * (((cos ((2 * x) + h)) - (cos h)) ^2)))
.= - ((1 / (1 / 4)) * (((sin ((2 * x) + h)) * (sin h)) / (((cos ((2 * x) + h)) - (cos h)) ^2))) by XCMPLX_1:76
.= - (((4 * (sin ((2 * x) + h))) * (sin h)) / (((cos ((2 * x) + h)) - (cos h)) ^2)) ;
hence  (fD ((cosec (#) cosec),h)) . x = - (((4 * (sin ((2 * x) + h))) * (sin h)) / (((cos ((2 * x) + h)) - (cos h)) ^2)) ; ::_thesis: verum
end;

theorem :: DIFF_4:12
for x, h being Real st x in dom cosec & x - h in dom cosec holds
(bD ((cosec (#) cosec),h)) . x = - (((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) - (cos h)) ^2))
proof
let x, h be Real; ::_thesis: ( x in dom cosec & x - h in dom cosec implies (bD ((cosec (#) cosec),h)) . x = - (((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) - (cos h)) ^2)) )
set f = cosec (#) cosec;
assume A1: ( x in dom cosec & x - h in dom cosec ) ; ::_thesis: (bD ((cosec (#) cosec),h)) . x = - (((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) - (cos h)) ^2))
A2: ( sin . x <> 0 & sin . (x - h) <> 0 ) by A1, RFUNCT_1:3;
 ( x in dom (cosec (#) cosec) & x - h in dom (cosec (#) cosec) )
proof
 ( x in (dom cosec) /\ (dom cosec) & x - h in (dom cosec) /\ (dom cosec) ) by A1;
hence  ( x in dom (cosec (#) cosec) & x - h in dom (cosec (#) cosec) ) by VALUED_1:def_4; ::_thesis: verum
end;
then (bD ((cosec (#) cosec),h)) . x = ((cosec (#) cosec) . x) - ((cosec (#) cosec) . (x - h)) by DIFF_1:38
.= ((cosec . x) * (cosec . x)) - ((cosec (#) cosec) . (x - h)) by VALUED_1:5
.= ((cosec . x) * (cosec . x)) - ((cosec . (x - h)) * (cosec . (x - h))) by VALUED_1:5
.= (((sin . x) ") * (cosec . x)) - ((cosec . (x - h)) * (cosec . (x - h))) by A1, RFUNCT_1:def_2
.= (((sin . x) ") * ((sin . x) ")) - ((cosec . (x - h)) * (cosec . (x - h))) by A1, RFUNCT_1:def_2
.= (((sin . x) ") * ((sin . x) ")) - (((sin . (x - h)) ") * (cosec . (x - h))) by A1, RFUNCT_1:def_2
.= (((sin . x) ") ^2) - (((sin . (x - h)) ") ^2) by A1, RFUNCT_1:def_2
.= ((1 / (sin . x)) - (1 / (sin . (x - h)))) * ((1 / (sin . x)) + (1 / (sin . (x - h))))
.= (((1 * (sin . (x - h))) - (1 * (sin . x))) / ((sin . x) * (sin . (x - h)))) * ((1 / (sin . x)) + (1 / (sin . (x - h)))) by A2, XCMPLX_1:130
.= (((sin . (x - h)) - (sin . x)) / ((sin . x) * (sin . (x - h)))) * (((sin . (x - h)) + (sin . x)) / ((sin . x) * (sin . (x - h)))) by A2, XCMPLX_1:116
.= (((sin . (x - h)) - (sin . x)) * ((sin . (x - h)) + (sin . x))) / (((sin . x) * (sin . (x - h))) * ((sin . x) * (sin . (x - h)))) by XCMPLX_1:76
.= (((sin (x - h)) * (sin (x - h))) - ((sin x) * (sin x))) / (((sin x) * (sin (x - h))) ^2)
.= ((sin ((x - h) + x)) * (sin ((x - h) - x))) / (((sin x) * (sin (x - h))) ^2) by SIN_COS4:37
.= ((sin ((2 * x) - h)) * (sin (- h))) / ((- ((1 / 2) * ((cos (x + (x - h))) - (cos (x - (x - h)))))) ^2) by SIN_COS4:29
.= ((sin ((2 * x) - h)) * (- (sin h))) / ((1 / 4) * (((cos ((2 * x) - h)) - (cos h)) ^2)) by SIN_COS:31
.= - ((1 * ((sin ((2 * x) - h)) * (sin h))) / ((1 / 4) * (((cos ((2 * x) - h)) - (cos h)) ^2)))
.= - ((1 / (1 / 4)) * (((sin ((2 * x) - h)) * (sin h)) / (((cos ((2 * x) - h)) - (cos h)) ^2))) by XCMPLX_1:76
.= - (((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) - (cos h)) ^2)) ;
hence  (bD ((cosec (#) cosec),h)) . x = - (((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) - (cos h)) ^2)) ; ::_thesis: verum
end;

theorem :: DIFF_4:13
for x, h being Real st x + (h / 2) in dom cosec & x - (h / 2) in dom cosec holds
(cD ((cosec (#) cosec),h)) . x = - (((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) - (cos h)) ^2))
proof
let x, h be Real; ::_thesis: ( x + (h / 2) in dom cosec & x - (h / 2) in dom cosec implies (cD ((cosec (#) cosec),h)) . x = - (((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) - (cos h)) ^2)) )
set f = cosec (#) cosec;
assume A1: ( x + (h / 2) in dom cosec & x - (h / 2) in dom cosec ) ; ::_thesis: (cD ((cosec (#) cosec),h)) . x = - (((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) - (cos h)) ^2))
A2: ( sin . (x + (h / 2)) <> 0 & sin . (x - (h / 2)) <> 0 ) by A1, RFUNCT_1:3;
 ( x + (h / 2) in dom (cosec (#) cosec) & x - (h / 2) in dom (cosec (#) cosec) )
proof
 ( x + (h / 2) in (dom cosec) /\ (dom cosec) & x - (h / 2) in (dom cosec) /\ (dom cosec) ) by A1;
hence  ( x + (h / 2) in dom (cosec (#) cosec) & x - (h / 2) in dom (cosec (#) cosec) ) by VALUED_1:def_4; ::_thesis: verum
end;
then (cD ((cosec (#) cosec),h)) . x = ((cosec (#) cosec) . (x + (h / 2))) - ((cosec (#) cosec) . (x - (h / 2))) by DIFF_1:39
.= ((cosec . (x + (h / 2))) * (cosec . (x + (h / 2)))) - ((cosec (#) cosec) . (x - (h / 2))) by VALUED_1:5
.= ((cosec . (x + (h / 2))) * (cosec . (x + (h / 2)))) - ((cosec . (x - (h / 2))) * (cosec . (x - (h / 2)))) by VALUED_1:5
.= (((sin . (x + (h / 2))) ") * (cosec . (x + (h / 2)))) - ((cosec . (x - (h / 2))) * (cosec . (x - (h / 2)))) by A1, RFUNCT_1:def_2
.= (((sin . (x + (h / 2))) ") * ((sin . (x + (h / 2))) ")) - ((cosec . (x - (h / 2))) * (cosec . (x - (h / 2)))) by A1, RFUNCT_1:def_2
.= (((sin . (x + (h / 2))) ") * ((sin . (x + (h / 2))) ")) - (((sin . (x - (h / 2))) ") * (cosec . (x - (h / 2)))) by A1, RFUNCT_1:def_2
.= (((sin . (x + (h / 2))) ") ^2) - (((sin . (x - (h / 2))) ") ^2) by A1, RFUNCT_1:def_2
.= ((1 / (sin . (x + (h / 2)))) - (1 / (sin . (x - (h / 2))))) * ((1 / (sin . (x + (h / 2)))) + (1 / (sin . (x - (h / 2)))))
.= (((1 * (sin . (x - (h / 2)))) - (1 * (sin . (x + (h / 2))))) / ((sin . (x + (h / 2))) * (sin . (x - (h / 2))))) * ((1 / (sin . (x + (h / 2)))) + (1 / (sin . (x - (h / 2))))) by A2, XCMPLX_1:130
.= (((sin . (x - (h / 2))) - (sin . (x + (h / 2)))) / ((sin . (x + (h / 2))) * (sin . (x - (h / 2))))) * (((sin . (x - (h / 2))) + (sin . (x + (h / 2)))) / ((sin . (x + (h / 2))) * (sin . (x - (h / 2))))) by A2, XCMPLX_1:116
.= (((sin . (x - (h / 2))) - (sin . (x + (h / 2)))) * ((sin . (x - (h / 2))) + (sin . (x + (h / 2))))) / (((sin . (x + (h / 2))) * (sin . (x - (h / 2)))) * ((sin . (x + (h / 2))) * (sin . (x - (h / 2))))) by XCMPLX_1:76
.= (((sin (x - (h / 2))) * (sin (x - (h / 2)))) - ((sin (x + (h / 2))) * (sin (x + (h / 2))))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2)
.= ((sin ((x - (h / 2)) + (x + (h / 2)))) * (sin ((x - (h / 2)) - (x + (h / 2))))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2) by SIN_COS4:37
.= ((sin (2 * x)) * (sin (- h))) / ((- ((1 / 2) * ((cos ((x + (h / 2)) + (x - (h / 2)))) - (cos ((x + (h / 2)) - (x - (h / 2))))))) ^2) by SIN_COS4:29
.= ((sin (2 * x)) * (- (sin h))) / ((1 / 4) * (((cos (2 * x)) - (cos h)) ^2)) by SIN_COS:31
.= - ((1 * ((sin (2 * x)) * (sin h))) / ((1 / 4) * (((cos (2 * x)) - (cos h)) ^2)))
.= - ((1 / (1 / 4)) * (((sin (2 * x)) * (sin h)) / (((cos (2 * x)) - (cos h)) ^2))) by XCMPLX_1:76
.= - (((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) - (cos h)) ^2)) ;
hence  (cD ((cosec (#) cosec),h)) . x = - (((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) - (cos h)) ^2)) ; ::_thesis: verum
end;

theorem :: DIFF_4:14
for x0, x1 being Real st x0 in dom sec & x1 in dom sec holds
[!(sec (#) sec),x0,x1!] = (4 * ((sin (x0 + x1)) * (sin (x0 - x1)))) / ((((cos (x0 + x1)) + (cos (x0 - x1))) ^2) * (x0 - x1))
proof
let x0, x1 be Real; ::_thesis: ( x0 in dom sec & x1 in dom sec implies [!(sec (#) sec),x0,x1!] = (4 * ((sin (x0 + x1)) * (sin (x0 - x1)))) / ((((cos (x0 + x1)) + (cos (x0 - x1))) ^2) * (x0 - x1)) )
assume A1: ( x0 in dom sec & x1 in dom sec ) ; ::_thesis: [!(sec (#) sec),x0,x1!] = (4 * ((sin (x0 + x1)) * (sin (x0 - x1)))) / ((((cos (x0 + x1)) + (cos (x0 - x1))) ^2) * (x0 - x1))
A2: ( cos . x0 <> 0 & cos . x1 <> 0 ) by A1, RFUNCT_1:3;
[!(sec (#) sec),x0,x1!] = (((sec . x0) * (sec . x0)) - ((sec (#) sec) . x1)) / (x0 - x1) by VALUED_1:5
.= (((sec . x0) * (sec . x0)) - ((sec . x1) * (sec . x1))) / (x0 - x1) by VALUED_1:5
.= ((((cos . x0) ") * (sec . x0)) - ((sec . x1) * (sec . x1))) / (x0 - x1) by A1, RFUNCT_1:def_2
.= ((((cos . x0) ") * ((cos . x0) ")) - ((sec . x1) * (sec . x1))) / (x0 - x1) by A1, RFUNCT_1:def_2
.= ((((cos . x0) ") * ((cos . x0) ")) - (((cos . x1) ") * (sec . x1))) / (x0 - x1) by A1, RFUNCT_1:def_2
.= ((((cos . x0) ") ^2) - (((cos . x1) ") ^2)) / (x0 - x1) by A1, RFUNCT_1:def_2
.= (((1 / (cos . x0)) - (1 / (cos . x1))) * ((1 / (cos . x0)) + (1 / (cos . x1)))) / (x0 - x1)
.= ((((1 * (cos . x1)) - (1 * (cos . x0))) / ((cos . x0) * (cos . x1))) * ((1 / (cos . x0)) + (1 / (cos . x1)))) / (x0 - x1) by A2, XCMPLX_1:130
.= ((((cos . x1) - (cos . x0)) / ((cos . x0) * (cos . x1))) * (((cos . x1) + (cos . x0)) / ((cos . x0) * (cos . x1)))) / (x0 - x1) by A2, XCMPLX_1:116
.= ((((cos . x1) - (cos . x0)) * ((cos . x1) + (cos . x0))) / (((cos . x0) * (cos . x1)) * ((cos . x0) * (cos . x1)))) / (x0 - x1) by XCMPLX_1:76
.= ((((cos x1) * (cos x1)) - ((cos x0) * (cos x0))) / (((cos x0) * (cos x1)) ^2)) / (x0 - x1)
.= (((sin (x0 + x1)) * (sin (x0 - x1))) / (((cos x0) * (cos x1)) ^2)) / (x0 - x1) by SIN_COS4:38
.= (((sin (x0 + x1)) * (sin (x0 - x1))) / (((1 / 2) * ((cos (x0 + x1)) + (cos (x0 - x1)))) ^2)) / (x0 - x1) by SIN_COS4:32
.= ((1 * ((sin (x0 + x1)) * (sin (x0 - x1)))) / ((1 / 4) * (((cos (x0 + x1)) + (cos (x0 - x1))) ^2))) / (x0 - x1)
.= ((1 / (1 / 4)) * (((sin (x0 + x1)) * (sin (x0 - x1))) / (((cos (x0 + x1)) + (cos (x0 - x1))) ^2))) / (x0 - x1) by XCMPLX_1:76
.= ((4 * ((sin (x0 + x1)) * (sin (x0 - x1)))) / (((cos (x0 + x1)) + (cos (x0 - x1))) ^2)) / (x0 - x1)
.= (4 * ((sin (x0 + x1)) * (sin (x0 - x1)))) / ((((cos (x0 + x1)) + (cos (x0 - x1))) ^2) * (x0 - x1)) by XCMPLX_1:78 ;
hence  [!(sec (#) sec),x0,x1!] = (4 * ((sin (x0 + x1)) * (sin (x0 - x1)))) / ((((cos (x0 + x1)) + (cos (x0 - x1))) ^2) * (x0 - x1)) ; ::_thesis: verum
end;

theorem :: DIFF_4:15
for x, h being Real st x in dom sec & x + h in dom sec holds
(fD ((sec (#) sec),h)) . x = ((4 * (sin ((2 * x) + h))) * (sin h)) / (((cos ((2 * x) + h)) + (cos h)) ^2)
proof
let x, h be Real; ::_thesis: ( x in dom sec & x + h in dom sec implies (fD ((sec (#) sec),h)) . x = ((4 * (sin ((2 * x) + h))) * (sin h)) / (((cos ((2 * x) + h)) + (cos h)) ^2) )
set f = sec (#) sec;
assume A1: ( x in dom sec & x + h in dom sec ) ; ::_thesis: (fD ((sec (#) sec),h)) . x = ((4 * (sin ((2 * x) + h))) * (sin h)) / (((cos ((2 * x) + h)) + (cos h)) ^2)
A2: ( cos . x <> 0 & cos . (x + h) <> 0 ) by A1, RFUNCT_1:3;
 ( x in dom (sec (#) sec) & x + h in dom (sec (#) sec) )
proof
 ( x in (dom sec) /\ (dom sec) & x + h in (dom sec) /\ (dom sec) ) by A1;
hence  ( x in dom (sec (#) sec) & x + h in dom (sec (#) sec) ) by VALUED_1:def_4; ::_thesis: verum
end;
then (fD ((sec (#) sec),h)) . x = ((sec (#) sec) . (x + h)) - ((sec (#) sec) . x) by DIFF_1:1
.= ((sec . (x + h)) * (sec . (x + h))) - ((sec (#) sec) . x) by VALUED_1:5
.= ((sec . (x + h)) * (sec . (x + h))) - ((sec . x) * (sec . x)) by VALUED_1:5
.= (((cos . (x + h)) ") * (sec . (x + h))) - ((sec . x) * (sec . x)) by A1, RFUNCT_1:def_2
.= (((cos . (x + h)) ") * ((cos . (x + h)) ")) - ((sec . x) * (sec . x)) by A1, RFUNCT_1:def_2
.= (((cos . (x + h)) ") * ((cos . (x + h)) ")) - (((cos . x) ") * (sec . x)) by A1, RFUNCT_1:def_2
.= (((cos . (x + h)) ") ^2) - (((cos . x) ") ^2) by A1, RFUNCT_1:def_2
.= ((1 / (cos . (x + h))) - (1 / (cos . x))) * ((1 / (cos . (x + h))) + (1 / (cos . x)))
.= (((1 * (cos . x)) - (1 * (cos . (x + h)))) / ((cos . (x + h)) * (cos . x))) * ((1 / (cos . (x + h))) + (1 / (cos . x))) by A2, XCMPLX_1:130
.= (((cos . x) - (cos . (x + h))) / ((cos . (x + h)) * (cos . x))) * (((cos . x) + (cos . (x + h))) / ((cos . (x + h)) * (cos . x))) by A2, XCMPLX_1:116
.= (((cos . x) - (cos . (x + h))) * ((cos . x) + (cos . (x + h)))) / (((cos . (x + h)) * (cos . x)) * ((cos . (x + h)) * (cos . x))) by XCMPLX_1:76
.= (((cos x) * (cos x)) - ((cos (x + h)) * (cos (x + h)))) / (((cos (x + h)) * (cos x)) ^2)
.= ((sin ((x + h) + x)) * (sin ((x + h) - x))) / (((cos (x + h)) * (cos x)) ^2) by SIN_COS4:38
.= ((sin ((2 * x) + h)) * (sin h)) / (((1 / 2) * ((cos ((x + h) + x)) + (cos ((x + h) - x)))) ^2) by SIN_COS4:32
.= (1 * ((sin ((2 * x) + h)) * (sin h))) / ((1 / 4) * (((cos ((2 * x) + h)) + (cos h)) ^2))
.= (1 / (1 / 4)) * (((sin ((2 * x) + h)) * (sin h)) / (((cos ((2 * x) + h)) + (cos h)) ^2)) by XCMPLX_1:76
.= ((4 * (sin ((2 * x) + h))) * (sin h)) / (((cos ((2 * x) + h)) + (cos h)) ^2) ;
hence  (fD ((sec (#) sec),h)) . x = ((4 * (sin ((2 * x) + h))) * (sin h)) / (((cos ((2 * x) + h)) + (cos h)) ^2) ; ::_thesis: verum
end;

theorem :: DIFF_4:16
for x, h being Real st x in dom sec & x - h in dom sec holds
(bD ((sec (#) sec),h)) . x = ((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) + (cos h)) ^2)
proof
let x, h be Real; ::_thesis: ( x in dom sec & x - h in dom sec implies (bD ((sec (#) sec),h)) . x = ((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) + (cos h)) ^2) )
set f = sec (#) sec;
assume A1: ( x in dom sec & x - h in dom sec ) ; ::_thesis: (bD ((sec (#) sec),h)) . x = ((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) + (cos h)) ^2)
A2: ( cos . x <> 0 & cos . (x - h) <> 0 ) by A1, RFUNCT_1:3;
 ( x in dom (sec (#) sec) & x - h in dom (sec (#) sec) )
proof
 ( x in (dom sec) /\ (dom sec) & x - h in (dom sec) /\ (dom sec) ) by A1;
hence  ( x in dom (sec (#) sec) & x - h in dom (sec (#) sec) ) by VALUED_1:def_4; ::_thesis: verum
end;
then (bD ((sec (#) sec),h)) . x = ((sec (#) sec) . x) - ((sec (#) sec) . (x - h)) by DIFF_1:38
.= ((sec . x) * (sec . x)) - ((sec (#) sec) . (x - h)) by VALUED_1:5
.= ((sec . x) * (sec . x)) - ((sec . (x - h)) * (sec . (x - h))) by VALUED_1:5
.= (((cos . x) ") * (sec . x)) - ((sec . (x - h)) * (sec . (x - h))) by A1, RFUNCT_1:def_2
.= (((cos . x) ") * ((cos . x) ")) - ((sec . (x - h)) * (sec . (x - h))) by A1, RFUNCT_1:def_2
.= (((cos . x) ") * ((cos . x) ")) - (((cos . (x - h)) ") * (sec . (x - h))) by A1, RFUNCT_1:def_2
.= (((cos . x) ") ^2) - (((cos . (x - h)) ") ^2) by A1, RFUNCT_1:def_2
.= ((1 / (cos . x)) - (1 / (cos . (x - h)))) * ((1 / (cos . x)) + (1 / (cos . (x - h))))
.= (((1 * (cos . (x - h))) - (1 * (cos . x))) / ((cos . x) * (cos . (x - h)))) * ((1 / (cos . x)) + (1 / (cos . (x - h)))) by A2, XCMPLX_1:130
.= (((cos . (x - h)) - (cos . x)) / ((cos . x) * (cos . (x - h)))) * (((cos . (x - h)) + (cos . x)) / ((cos . x) * (cos . (x - h)))) by A2, XCMPLX_1:116
.= (((cos . (x - h)) - (cos . x)) * ((cos . (x - h)) + (cos . x))) / (((cos . x) * (cos . (x - h))) * ((cos . x) * (cos . (x - h)))) by XCMPLX_1:76
.= (((cos (x - h)) * (cos (x - h))) - ((cos x) * (cos x))) / (((cos x) * (cos (x - h))) ^2)
.= ((sin (x + (x - h))) * (sin (x - (x - h)))) / (((cos x) * (cos (x - h))) ^2) by SIN_COS4:38
.= ((sin ((2 * x) - h)) * (sin h)) / (((1 / 2) * ((cos (x + (x - h))) + (cos (x - (x - h))))) ^2) by SIN_COS4:32
.= (1 * ((sin ((2 * x) - h)) * (sin h))) / ((1 / 4) * (((cos ((2 * x) - h)) + (cos h)) ^2))
.= (1 / (1 / 4)) * (((sin ((2 * x) - h)) * (sin h)) / (((cos ((2 * x) - h)) + (cos h)) ^2)) by XCMPLX_1:76
.= ((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) + (cos h)) ^2) ;
hence  (bD ((sec (#) sec),h)) . x = ((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) + (cos h)) ^2) ; ::_thesis: verum
end;

theorem :: DIFF_4:17
for x, h being Real st x + (h / 2) in dom sec & x - (h / 2) in dom sec holds
(cD ((sec (#) sec),h)) . x = ((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) + (cos h)) ^2)
proof
let x, h be Real; ::_thesis: ( x + (h / 2) in dom sec & x - (h / 2) in dom sec implies (cD ((sec (#) sec),h)) . x = ((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) + (cos h)) ^2) )
set f = sec (#) sec;
assume A1: ( x + (h / 2) in dom sec & x - (h / 2) in dom sec ) ; ::_thesis: (cD ((sec (#) sec),h)) . x = ((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) + (cos h)) ^2)
A2: ( cos . (x + (h / 2)) <> 0 & cos . (x - (h / 2)) <> 0 ) by A1, RFUNCT_1:3;
 ( x + (h / 2) in dom (sec (#) sec) & x - (h / 2) in dom (sec (#) sec) )
proof
 ( x + (h / 2) in (dom sec) /\ (dom sec) & x - (h / 2) in (dom sec) /\ (dom sec) ) by A1;
hence  ( x + (h / 2) in dom (sec (#) sec) & x - (h / 2) in dom (sec (#) sec) ) by VALUED_1:def_4; ::_thesis: verum
end;
then (cD ((sec (#) sec),h)) . x = ((sec (#) sec) . (x + (h / 2))) - ((sec (#) sec) . (x - (h / 2))) by DIFF_1:39
.= ((sec . (x + (h / 2))) * (sec . (x + (h / 2)))) - ((sec (#) sec) . (x - (h / 2))) by VALUED_1:5
.= ((sec . (x + (h / 2))) * (sec . (x + (h / 2)))) - ((sec . (x - (h / 2))) * (sec . (x - (h / 2)))) by VALUED_1:5
.= (((cos . (x + (h / 2))) ") * (sec . (x + (h / 2)))) - ((sec . (x - (h / 2))) * (sec . (x - (h / 2)))) by A1, RFUNCT_1:def_2
.= (((cos . (x + (h / 2))) ") * ((cos . (x + (h / 2))) ")) - ((sec . (x - (h / 2))) * (sec . (x - (h / 2)))) by A1, RFUNCT_1:def_2
.= (((cos . (x + (h / 2))) ") * ((cos . (x + (h / 2))) ")) - (((cos . (x - (h / 2))) ") * (sec . (x - (h / 2)))) by A1, RFUNCT_1:def_2
.= (((cos . (x + (h / 2))) ") ^2) - (((cos . (x - (h / 2))) ") ^2) by A1, RFUNCT_1:def_2
.= ((1 / (cos . (x + (h / 2)))) - (1 / (cos . (x - (h / 2))))) * ((1 / (cos . (x + (h / 2)))) + (1 / (cos . (x - (h / 2)))))
.= (((1 * (cos . (x - (h / 2)))) - (1 * (cos . (x + (h / 2))))) / ((cos . (x + (h / 2))) * (cos . (x - (h / 2))))) * ((1 / (cos . (x + (h / 2)))) + (1 / (cos . (x - (h / 2))))) by A2, XCMPLX_1:130
.= (((cos . (x - (h / 2))) - (cos . (x + (h / 2)))) / ((cos . (x + (h / 2))) * (cos . (x - (h / 2))))) * (((cos . (x - (h / 2))) + (cos . (x + (h / 2)))) / ((cos . (x + (h / 2))) * (cos . (x - (h / 2))))) by A2, XCMPLX_1:116
.= (((cos . (x - (h / 2))) - (cos . (x + (h / 2)))) * ((cos . (x - (h / 2))) + (cos . (x + (h / 2))))) / (((cos . (x + (h / 2))) * (cos . (x - (h / 2)))) * ((cos . (x + (h / 2))) * (cos . (x - (h / 2))))) by XCMPLX_1:76
.= (((cos (x - (h / 2))) * (cos (x - (h / 2)))) - ((cos (x + (h / 2))) * (cos (x + (h / 2))))) / (((cos (x + (h / 2))) * (cos (x - (h / 2)))) ^2)
.= ((sin ((x + (h / 2)) + (x - (h / 2)))) * (sin ((x + (h / 2)) - (x - (h / 2))))) / (((cos (x + (h / 2))) * (cos (x - (h / 2)))) ^2) by SIN_COS4:38
.= ((sin (2 * x)) * (sin h)) / (((1 / 2) * ((cos ((x + (h / 2)) + (x - (h / 2)))) + (cos ((x + (h / 2)) - (x - (h / 2)))))) ^2) by SIN_COS4:32
.= (1 * ((sin (2 * x)) * (sin h))) / ((1 / 4) * (((cos (2 * x)) + (cos h)) ^2))
.= (1 / (1 / 4)) * (((sin (2 * x)) * (sin h)) / (((cos (2 * x)) + (cos h)) ^2)) by XCMPLX_1:76
.= ((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) + (cos h)) ^2) ;
hence  (cD ((sec (#) sec),h)) . x = ((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) + (cos h)) ^2) ; ::_thesis: verum
end;

theorem :: DIFF_4:18
for x0, x1 being Real st x0 in (dom cosec) /\ (dom sec) & x1 in (dom cosec) /\ (dom sec) holds
[!(cosec (#) sec),x0,x1!] = ((4 * ((cos (x1 + x0)) * (sin (x1 - x0)))) / ((sin (2 * x0)) * (sin (2 * x1)))) / (x0 - x1)
proof
let x0, x1 be Real; ::_thesis: ( x0 in (dom cosec) /\ (dom sec) & x1 in (dom cosec) /\ (dom sec) implies [!(cosec (#) sec),x0,x1!] = ((4 * ((cos (x1 + x0)) * (sin (x1 - x0)))) / ((sin (2 * x0)) * (sin (2 * x1)))) / (x0 - x1) )
assume A1: ( x0 in (dom cosec) /\ (dom sec) & x1 in (dom cosec) /\ (dom sec) ) ; ::_thesis: [!(cosec (#) sec),x0,x1!] = ((4 * ((cos (x1 + x0)) * (sin (x1 - x0)))) / ((sin (2 * x0)) * (sin (2 * x1)))) / (x0 - x1)
A2: ( x0 in dom cosec & x0 in dom sec ) by A1, XBOOLE_0:def_4;
A3: ( x1 in dom cosec & x1 in dom sec ) by A1, XBOOLE_0:def_4;
A4: ( sin . x0 <> 0 & cos . x0 <> 0 ) by A2, RFUNCT_1:3;
A5: ( sin . x1 <> 0 & cos . x1 <> 0 ) by A3, RFUNCT_1:3;
[!(cosec (#) sec),x0,x1!] = (((cosec . x0) * (sec . x0)) - ((cosec (#) sec) . x1)) / (x0 - x1) by VALUED_1:5
.= (((cosec . x0) * (sec . x0)) - ((cosec . x1) * (sec . x1))) / (x0 - x1) by VALUED_1:5
.= ((((sin . x0) ") * (sec . x0)) - ((cosec . x1) * (sec . x1))) / (x0 - x1) by A2, RFUNCT_1:def_2
.= ((((sin . x0) ") * ((cos . x0) ")) - ((cosec . x1) * (sec . x1))) / (x0 - x1) by A2, RFUNCT_1:def_2
.= ((((sin . x0) ") * ((cos . x0) ")) - (((sin . x1) ") * (sec . x1))) / (x0 - x1) by A3, RFUNCT_1:def_2
.= ((((sin . x0) ") * ((cos . x0) ")) - (((sin . x1) ") * ((cos . x1) "))) / (x0 - x1) by A3, RFUNCT_1:def_2
.= ((((sin . x0) * (cos . x0)) ") - (((sin . x1) ") * ((cos . x1) "))) / (x0 - x1) by XCMPLX_1:204
.= ((1 / ((sin . x0) * (cos . x0))) - (1 / ((sin . x1) * (cos . x1)))) / (x0 - x1) by XCMPLX_1:204
.= (((1 * ((sin . x1) * (cos . x1))) - (1 * ((sin . x0) * (cos . x0)))) / (((sin . x0) * (cos . x0)) * ((sin . x1) * (cos . x1)))) / (x0 - x1) by A4, A5, XCMPLX_1:130
.= (((cos (x1 + x0)) * (sin (x1 - x0))) / (((1 / 2) * ((2 * (sin x0)) * (cos x0))) * ((1 / 2) * ((2 * (sin x1)) * (cos x1))))) / (x0 - x1) by SIN_COS4:40
.= (((cos (x1 + x0)) * (sin (x1 - x0))) / (((1 / 2) * (sin (2 * x0))) * ((1 / 2) * ((2 * (sin x1)) * (cos x1))))) / (x0 - x1) by SIN_COS5:5
.= (((cos (x1 + x0)) * (sin (x1 - x0))) / (((1 / 2) * (sin (2 * x0))) * ((1 / 2) * (sin (2 * x1))))) / (x0 - x1) by SIN_COS5:5
.= (((cos (x1 + x0)) * (sin (x1 - x0))) / ((((sin (2 * x0)) * (sin (2 * x1))) * 1) / 4)) / (x0 - x1)
.= ((1 / (1 / 4)) * (((cos (x1 + x0)) * (sin (x1 - x0))) / ((sin (2 * x0)) * (sin (2 * x1))))) / (x0 - x1) by XCMPLX_1:103
.= ((4 * ((cos (x1 + x0)) * (sin (x1 - x0)))) / ((sin (2 * x0)) * (sin (2 * x1)))) / (x0 - x1) ;
hence  [!(cosec (#) sec),x0,x1!] = ((4 * ((cos (x1 + x0)) * (sin (x1 - x0)))) / ((sin (2 * x0)) * (sin (2 * x1)))) / (x0 - x1) ; ::_thesis: verum
end;

theorem :: DIFF_4:19
for x, h being Real st x + h in (dom cosec) /\ (dom sec) & x in (dom cosec) /\ (dom sec) holds
(fD ((cosec (#) sec),h)) . x = - (4 * (((cos ((2 * x) + h)) * (sin h)) / ((sin (2 * (x + h))) * (sin (2 * x)))))
proof
let x, h be Real; ::_thesis: ( x + h in (dom cosec) /\ (dom sec) & x in (dom cosec) /\ (dom sec) implies (fD ((cosec (#) sec),h)) . x = - (4 * (((cos ((2 * x) + h)) * (sin h)) / ((sin (2 * (x + h))) * (sin (2 * x))))) )
set f = cosec (#) sec;
assume A1: ( x + h in (dom cosec) /\ (dom sec) & x in (dom cosec) /\ (dom sec) ) ; ::_thesis: (fD ((cosec (#) sec),h)) . x = - (4 * (((cos ((2 * x) + h)) * (sin h)) / ((sin (2 * (x + h))) * (sin (2 * x)))))
A2: ( x + h in dom cosec & x + h in dom sec ) by A1, XBOOLE_0:def_4;
A3: ( x in dom cosec & x in dom sec ) by A1, XBOOLE_0:def_4;
A4: ( sin . (x + h) <> 0 & cos . (x + h) <> 0 ) by A2, RFUNCT_1:3;
A5: ( sin . x <> 0 & cos . x <> 0 ) by A3, RFUNCT_1:3;
 ( x in dom (cosec (#) sec) & x + h in dom (cosec (#) sec) ) by A1, VALUED_1:def_4;
then (fD ((cosec (#) sec),h)) . x = ((cosec (#) sec) . (x + h)) - ((cosec (#) sec) . x) by DIFF_1:1
.= ((cosec . (x + h)) * (sec . (x + h))) - ((cosec (#) sec) . x) by VALUED_1:5
.= ((cosec . (x + h)) * (sec . (x + h))) - ((cosec . x) * (sec . x)) by VALUED_1:5
.= (((sin . (x + h)) ") * (sec . (x + h))) - ((cosec . x) * (sec . x)) by A2, RFUNCT_1:def_2
.= (((sin . (x + h)) ") * ((cos . (x + h)) ")) - ((cosec . x) * (sec . x)) by A2, RFUNCT_1:def_2
.= (((sin . (x + h)) ") * ((cos . (x + h)) ")) - (((sin . x) ") * (sec . x)) by A3, RFUNCT_1:def_2
.= (((sin . (x + h)) ") * ((cos . (x + h)) ")) - (((sin . x) ") * ((cos . x) ")) by A3, RFUNCT_1:def_2
.= (((sin . (x + h)) * (cos . (x + h))) ") - (((sin . x) ") * ((cos . x) ")) by XCMPLX_1:204
.= (1 / ((sin . (x + h)) * (cos . (x + h)))) - (1 / ((sin . x) * (cos . x))) by XCMPLX_1:204
.= ((1 * ((sin . x) * (cos . x))) - (1 * ((sin . (x + h)) * (cos . (x + h))))) / (((sin . (x + h)) * (cos . (x + h))) * ((sin . x) * (cos . x))) by A4, A5, XCMPLX_1:130
.= ((cos (x + (x + h))) * (sin (x - (x + h)))) / (((sin (x + h)) * (cos (x + h))) * ((sin x) * (cos x))) by SIN_COS4:40
.= ((cos ((2 * x) + h)) * (sin (- h))) / (((1 * (sin (x + h))) * (cos (x + h))) * ((1 * (sin x)) * (cos x)))
.= ((cos ((2 * x) + h)) * (- (sin h))) / (((((1 / 2) * 2) * (sin (x + h))) * (cos (x + h))) * ((((1 / 2) * 2) * (sin x)) * (cos x))) by SIN_COS:31
.= (- ((cos ((2 * x) + h)) * (sin h))) / (((1 / 2) * ((2 * (sin (x + h))) * (cos (x + h)))) * ((1 / 2) * ((2 * (sin x)) * (cos x))))
.= (- ((cos ((2 * x) + h)) * (sin h))) / (((1 / 2) * (sin (2 * (x + h)))) * ((1 / 2) * ((2 * (sin x)) * (cos x)))) by SIN_COS5:5
.= (- ((cos ((2 * x) + h)) * (sin h))) / (((1 / 2) * (sin (2 * (x + h)))) * ((1 / 2) * (sin (2 * x)))) by SIN_COS5:5
.= - (((cos ((2 * x) + h)) * (sin h)) / (((sin (2 * (x + h))) * (sin (2 * x))) * (1 / 4)))
.= - ((1 / (1 / 4)) * (((cos ((2 * x) + h)) * (sin h)) / ((sin (2 * (x + h))) * (sin (2 * x))))) by XCMPLX_1:103
.= - (4 * (((cos ((2 * x) + h)) * (sin h)) / ((sin (2 * (x + h))) * (sin (2 * x))))) ;
hence  (fD ((cosec (#) sec),h)) . x = - (4 * (((cos ((2 * x) + h)) * (sin h)) / ((sin (2 * (x + h))) * (sin (2 * x))))) ; ::_thesis: verum
end;

theorem :: DIFF_4:20
for x, h being Real st x - h in (dom cosec) /\ (dom sec) & x in (dom cosec) /\ (dom sec) holds
(bD ((cosec (#) sec),h)) . x = - (4 * (((cos ((2 * x) - h)) * (sin h)) / ((sin (2 * x)) * (sin (2 * (x - h))))))
proof
let x, h be Real; ::_thesis: ( x - h in (dom cosec) /\ (dom sec) & x in (dom cosec) /\ (dom sec) implies (bD ((cosec (#) sec),h)) . x = - (4 * (((cos ((2 * x) - h)) * (sin h)) / ((sin (2 * x)) * (sin (2 * (x - h)))))) )
set f = cosec (#) sec;
assume A1: ( x - h in (dom cosec) /\ (dom sec) & x in (dom cosec) /\ (dom sec) ) ; ::_thesis: (bD ((cosec (#) sec),h)) . x = - (4 * (((cos ((2 * x) - h)) * (sin h)) / ((sin (2 * x)) * (sin (2 * (x - h))))))
A2: ( x - h in dom cosec & x - h in dom sec ) by A1, XBOOLE_0:def_4;
A3: ( x in dom cosec & x in dom sec ) by A1, XBOOLE_0:def_4;
A4: ( sin . (x - h) <> 0 & cos . (x - h) <> 0 ) by A2, RFUNCT_1:3;
A5: ( sin . x <> 0 & cos . x <> 0 ) by A3, RFUNCT_1:3;
 ( x in dom (cosec (#) sec) & x - h in dom (cosec (#) sec) ) by A1, VALUED_1:def_4;
then (bD ((cosec (#) sec),h)) . x = ((cosec (#) sec) . x) - ((cosec (#) sec) . (x - h)) by DIFF_1:38
.= ((cosec . x) * (sec . x)) - ((cosec (#) sec) . (x - h)) by VALUED_1:5
.= ((cosec . x) * (sec . x)) - ((cosec . (x - h)) * (sec . (x - h))) by VALUED_1:5
.= (((sin . x) ") * (sec . x)) - ((cosec . (x - h)) * (sec . (x - h))) by A3, RFUNCT_1:def_2
.= (((sin . x) ") * ((cos . x) ")) - ((cosec . (x - h)) * (sec . (x - h))) by A3, RFUNCT_1:def_2
.= (((sin . x) ") * ((cos . x) ")) - (((sin . (x - h)) ") * (sec . (x - h))) by A2, RFUNCT_1:def_2
.= (((sin . x) ") * ((cos . x) ")) - (((sin . (x - h)) ") * ((cos . (x - h)) ")) by A2, RFUNCT_1:def_2
.= (((sin . x) * (cos . x)) ") - (((sin . (x - h)) ") * ((cos . (x - h)) ")) by XCMPLX_1:204
.= (1 / ((sin . x) * (cos . x))) - (1 / ((sin . (x - h)) * (cos . (x - h)))) by XCMPLX_1:204
.= ((1 * ((sin . (x - h)) * (cos . (x - h)))) - (1 * ((sin . x) * (cos . x)))) / (((sin . x) * (cos . x)) * ((sin . (x - h)) * (cos . (x - h)))) by A4, A5, XCMPLX_1:130
.= ((cos ((x - h) + x)) * (sin ((x - h) - x))) / (((sin x) * (cos x)) * ((sin (x - h)) * (cos (x - h)))) by SIN_COS4:40
.= ((cos ((2 * x) - h)) * (- (sin h))) / (((((1 / 2) * 2) * (sin x)) * (cos x)) * ((((1 / 2) * 2) * (sin (x - h))) * (cos (x - h)))) by SIN_COS:31
.= (- ((cos ((2 * x) - h)) * (sin h))) / (((1 / 2) * ((2 * (sin x)) * (cos x))) * ((1 / 2) * ((2 * (sin (x - h))) * (cos (x - h)))))
.= (- ((cos ((2 * x) - h)) * (sin h))) / (((1 / 2) * (sin (2 * x))) * ((1 / 2) * ((2 * (sin (x - h))) * (cos (x - h))))) by SIN_COS5:5
.= (- ((cos ((2 * x) - h)) * (sin h))) / (((1 / 2) * (sin (2 * x))) * ((1 / 2) * (sin (2 * (x - h))))) by SIN_COS5:5
.= - (((cos ((2 * x) - h)) * (sin h)) / (((sin (2 * x)) * (sin (2 * (x - h)))) * (1 / 4)))
.= - ((1 / (1 / 4)) * (((cos ((2 * x) - h)) * (sin h)) / ((sin (2 * x)) * (sin (2 * (x - h)))))) by XCMPLX_1:103
.= - (4 * (((cos ((2 * x) - h)) * (sin h)) / ((sin (2 * x)) * (sin (2 * (x - h)))))) ;
hence  (bD ((cosec (#) sec),h)) . x = - (4 * (((cos ((2 * x) - h)) * (sin h)) / ((sin (2 * x)) * (sin (2 * (x - h)))))) ; ::_thesis: verum
end;

theorem :: DIFF_4:21
for x, h being Real st x + (h / 2) in (dom cosec) /\ (dom sec) & x - (h / 2) in (dom cosec) /\ (dom sec) holds
(cD ((cosec (#) sec),h)) . x = - (4 * (((cos (2 * x)) * (sin h)) / ((sin ((2 * x) + h)) * (sin ((2 * x) - h)))))
proof
let x, h be Real; ::_thesis: ( x + (h / 2) in (dom cosec) /\ (dom sec) & x - (h / 2) in (dom cosec) /\ (dom sec) implies (cD ((cosec (#) sec),h)) . x = - (4 * (((cos (2 * x)) * (sin h)) / ((sin ((2 * x) + h)) * (sin ((2 * x) - h))))) )
set f = cosec (#) sec;
assume A1: ( x + (h / 2) in (dom cosec) /\ (dom sec) & x - (h / 2) in (dom cosec) /\ (dom sec) ) ; ::_thesis: (cD ((cosec (#) sec),h)) . x = - (4 * (((cos (2 * x)) * (sin h)) / ((sin ((2 * x) + h)) * (sin ((2 * x) - h)))))
A2: ( x + (h / 2) in dom cosec & x + (h / 2) in dom sec ) by A1, XBOOLE_0:def_4;
A3: ( x - (h / 2) in dom cosec & x - (h / 2) in dom sec ) by A1, XBOOLE_0:def_4;
A4: ( sin . (x + (h / 2)) <> 0 & cos . (x + (h / 2)) <> 0 ) by A2, RFUNCT_1:3;
A5: ( sin . (x - (h / 2)) <> 0 & cos . (x - (h / 2)) <> 0 ) by A3, RFUNCT_1:3;
 ( x + (h / 2) in dom (cosec (#) sec) & x - (h / 2) in dom (cosec (#) sec) ) by A1, VALUED_1:def_4;
then (cD ((cosec (#) sec),h)) . x = ((cosec (#) sec) . (x + (h / 2))) - ((cosec (#) sec) . (x - (h / 2))) by DIFF_1:39
.= ((cosec . (x + (h / 2))) * (sec . (x + (h / 2)))) - ((cosec (#) sec) . (x - (h / 2))) by VALUED_1:5
.= ((cosec . (x + (h / 2))) * (sec . (x + (h / 2)))) - ((cosec . (x - (h / 2))) * (sec . (x - (h / 2)))) by VALUED_1:5
.= (((sin . (x + (h / 2))) ") * (sec . (x + (h / 2)))) - ((cosec . (x - (h / 2))) * (sec . (x - (h / 2)))) by A2, RFUNCT_1:def_2
.= (((sin . (x + (h / 2))) ") * ((cos . (x + (h / 2))) ")) - ((cosec . (x - (h / 2))) * (sec . (x - (h / 2)))) by A2, RFUNCT_1:def_2
.= (((sin . (x + (h / 2))) ") * ((cos . (x + (h / 2))) ")) - (((sin . (x - (h / 2))) ") * (sec . (x - (h / 2)))) by A3, RFUNCT_1:def_2
.= (((sin . (x + (h / 2))) ") * ((cos . (x + (h / 2))) ")) - (((sin . (x - (h / 2))) ") * ((cos . (x - (h / 2))) ")) by A3, RFUNCT_1:def_2
.= (((sin . (x + (h / 2))) * (cos . (x + (h / 2)))) ") - (((sin . (x - (h / 2))) ") * ((cos . (x - (h / 2))) ")) by XCMPLX_1:204
.= (1 / ((sin . (x + (h / 2))) * (cos . (x + (h / 2))))) - (1 / ((sin . (x - (h / 2))) * (cos . (x - (h / 2))))) by XCMPLX_1:204
.= ((1 * ((sin . (x - (h / 2))) * (cos . (x - (h / 2))))) - (1 * ((sin . (x + (h / 2))) * (cos . (x + (h / 2)))))) / (((sin . (x + (h / 2))) * (cos . (x + (h / 2)))) * ((sin . (x - (h / 2))) * (cos . (x - (h / 2))))) by A4, A5, XCMPLX_1:130
.= ((cos ((x - (h / 2)) + (x + (h / 2)))) * (sin ((x - (h / 2)) - (x + (h / 2))))) / (((sin (x + (h / 2))) * (cos (x + (h / 2)))) * ((sin (x - (h / 2))) * (cos (x - (h / 2))))) by SIN_COS4:40
.= ((cos (2 * x)) * (sin (- h))) / (((1 * (sin (x + (h / 2)))) * (cos (x + (h / 2)))) * ((1 * (sin (x - (h / 2)))) * (cos (x - (h / 2)))))
.= ((cos (2 * x)) * (- (sin h))) / (((((1 / 2) * 2) * (sin (x + (h / 2)))) * (cos (x + (h / 2)))) * ((((1 / 2) * 2) * (sin (x - (h / 2)))) * (cos (x - (h / 2))))) by SIN_COS:31
.= (- ((cos (2 * x)) * (sin h))) / (((1 / 2) * ((2 * (sin (x + (h / 2)))) * (cos (x + (h / 2))))) * ((1 / 2) * ((2 * (sin (x - (h / 2)))) * (cos (x - (h / 2))))))
.= (- ((cos (2 * x)) * (sin h))) / (((1 / 2) * (sin (2 * (x + (h / 2))))) * ((1 / 2) * ((2 * (sin (x - (h / 2)))) * (cos (x - (h / 2)))))) by SIN_COS5:5
.= (- ((cos (2 * x)) * (sin h))) / (((1 / 2) * (sin (2 * (x + (h / 2))))) * ((1 / 2) * (sin (2 * (x - (h / 2)))))) by SIN_COS5:5
.= - (((cos (2 * x)) * (sin h)) / (((sin ((2 * x) + h)) * (sin ((2 * x) - h))) * (1 / 4)))
.= - ((1 / (1 / 4)) * (((cos (2 * x)) * (sin h)) / ((sin ((2 * x) + h)) * (sin ((2 * x) - h))))) by XCMPLX_1:103
.= - (4 * (((cos (2 * x)) * (sin h)) / ((sin ((2 * x) + h)) * (sin ((2 * x) - h))))) ;
hence  (cD ((cosec (#) sec),h)) . x = - (4 * (((cos (2 * x)) * (sin h)) / ((sin ((2 * x) + h)) * (sin ((2 * x) - h))))) ; ::_thesis: verum
end;

theorem :: DIFF_4:22
for x0, x1 being Real st x0 in dom tan & x1 in dom tan holds
[!((tan (#) tan) (#) cos),x0,x1!] = [!(tan (#) sin),x0,x1!]
proof
let x0, x1 be Real; ::_thesis: ( x0 in dom tan & x1 in dom tan implies [!((tan (#) tan) (#) cos),x0,x1!] = [!(tan (#) sin),x0,x1!] )
assume A1: ( x0 in dom tan & x1 in dom tan ) ; ::_thesis: [!((tan (#) tan) (#) cos),x0,x1!] = [!(tan (#) sin),x0,x1!]
[!((tan (#) tan) (#) cos),x0,x1!] = ((((tan (#) tan) . x0) * (cos . x0)) - (((tan (#) tan) (#) cos) . x1)) / (x0 - x1) by VALUED_1:5
.= ((((tan . x0) * (tan . x0)) * (cos . x0)) - (((tan (#) tan) (#) cos) . x1)) / (x0 - x1) by VALUED_1:5
.= ((((tan . x0) * (tan . x0)) * (cos . x0)) - (((tan (#) tan) . x1) * (cos . x1))) / (x0 - x1) by VALUED_1:5
.= ((((tan . x0) * (tan . x0)) * (cos . x0)) - (((tan . x1) * (tan . x1)) * (cos . x1))) / (x0 - x1) by VALUED_1:5
.= (((((sin . x0) * ((cos . x0) ")) * (tan . x0)) * (cos . x0)) - (((tan . x1) * (tan . x1)) * (cos . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1
.= (((((sin . x0) * ((cos . x0) ")) * (tan . x0)) * (cos . x0)) - ((((sin . x1) * ((cos . x1) ")) * (tan . x1)) * (cos . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1
.= ((((sin . x0) * ((cos . x0) * (1 / (cos . x0)))) * (tan . x0)) - (((sin . x1) * ((cos . x1) * (1 / (cos . x1)))) * (tan . x1))) / (x0 - x1)
.= ((((sin . x0) * 1) * (tan . x0)) - (((sin . x1) * ((cos . x1) * (1 / (cos . x1)))) * (tan . x1))) / (x0 - x1) by A1, FDIFF_8:1, XCMPLX_1:106
.= ((((sin . x0) * 1) * (tan . x0)) - (((sin . x1) * 1) * (tan . x1))) / (x0 - x1) by A1, FDIFF_8:1, XCMPLX_1:106
.= (((tan (#) sin) . x0) - ((tan . x1) * (sin . x1))) / (x0 - x1) by VALUED_1:5
.= [!(tan (#) sin),x0,x1!] by VALUED_1:5 ;
hence  [!((tan (#) tan) (#) cos),x0,x1!] = [!(tan (#) sin),x0,x1!] ; ::_thesis: verum
end;

theorem :: DIFF_4:23
for x, h being Real st x in dom tan & x + h in dom tan holds
(fD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + h)) - ((tan (#) sin) . x)
proof
let x, h be Real; ::_thesis: ( x in dom tan & x + h in dom tan implies (fD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + h)) - ((tan (#) sin) . x) )
set f = (tan (#) tan) (#) cos;
assume A1: ( x in dom tan & x + h in dom tan ) ; ::_thesis: (fD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + h)) - ((tan (#) sin) . x)
 ( x in dom ((tan (#) tan) (#) cos) & x + h in dom ((tan (#) tan) (#) cos) )
proof
set f1 = tan (#) tan;
set f2 = cos ;
A2: ( x in dom (tan (#) tan) & x + h in dom (tan (#) tan) )
proof
 ( x in (dom tan) /\ (dom tan) & x + h in (dom tan) /\ (dom tan) ) by A1;
hence  ( x in dom (tan (#) tan) & x + h in dom (tan (#) tan) ) by VALUED_1:def_4; ::_thesis: verum
end;
 ( x in (dom (tan (#) tan)) /\ (dom cos) & x + h in (dom (tan (#) tan)) /\ (dom cos) ) by A2, SIN_COS:24, XBOOLE_0:def_4;
hence  ( x in dom ((tan (#) tan) (#) cos) & x + h in dom ((tan (#) tan) (#) cos) ) by VALUED_1:def_4; ::_thesis: verum
end;
then (fD (((tan (#) tan) (#) cos),h)) . x = (((tan (#) tan) (#) cos) . (x + h)) - (((tan (#) tan) (#) cos) . x) by DIFF_1:1
.= (((tan (#) tan) . (x + h)) * (cos . (x + h))) - (((tan (#) tan) (#) cos) . x) by VALUED_1:5
.= (((tan . (x + h)) * (tan . (x + h))) * (cos . (x + h))) - (((tan (#) tan) (#) cos) . x) by VALUED_1:5
.= (((tan . (x + h)) * (tan . (x + h))) * (cos . (x + h))) - (((tan (#) tan) . x) * (cos . x)) by VALUED_1:5
.= (((tan . (x + h)) * (tan . (x + h))) * (cos . (x + h))) - (((tan . x) * (tan . x)) * (cos . x)) by VALUED_1:5
.= ((((sin . (x + h)) * ((cos . (x + h)) ")) * (tan . (x + h))) * (cos . (x + h))) - (((tan . x) * (tan . x)) * (cos . x)) by A1, RFUNCT_1:def_1
.= ((((sin . (x + h)) * ((cos . (x + h)) ")) * (tan . (x + h))) * (cos . (x + h))) - ((((sin . x) * ((cos . x) ")) * (tan . x)) * (cos . x)) by A1, RFUNCT_1:def_1
.= (((sin . (x + h)) * (tan . (x + h))) * ((cos . (x + h)) * (1 / (cos . (x + h))))) - (((sin . x) * (tan . x)) * ((cos . x) * (1 / (cos . x))))
.= (((sin . (x + h)) * (tan . (x + h))) * 1) - (((sin . x) * (tan . x)) * ((cos . x) * (1 / (cos . x)))) by A1, FDIFF_8:1, XCMPLX_1:106
.= (((sin . (x + h)) * (tan . (x + h))) * 1) - (((sin . x) * (tan . x)) * 1) by A1, FDIFF_8:1, XCMPLX_1:106
.= ((tan (#) sin) . (x + h)) - ((tan . x) * (sin . x)) by VALUED_1:5
.= ((tan (#) sin) . (x + h)) - ((tan (#) sin) . x) by VALUED_1:5 ;
hence  (fD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + h)) - ((tan (#) sin) . x) ; ::_thesis: verum
end;

theorem :: DIFF_4:24
for x, h being Real st x in dom tan & x - h in dom tan holds
(bD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . x) - ((tan (#) sin) . (x - h))
proof
let x, h be Real; ::_thesis: ( x in dom tan & x - h in dom tan implies (bD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . x) - ((tan (#) sin) . (x - h)) )
set f = (tan (#) tan) (#) cos;
assume A1: ( x in dom tan & x - h in dom tan ) ; ::_thesis: (bD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . x) - ((tan (#) sin) . (x - h))
 ( x in dom ((tan (#) tan) (#) cos) & x - h in dom ((tan (#) tan) (#) cos) )
proof
set f1 = tan (#) tan;
set f2 = cos ;
A2: ( x in dom (tan (#) tan) & x - h in dom (tan (#) tan) )
proof
 ( x in (dom tan) /\ (dom tan) & x - h in (dom tan) /\ (dom tan) ) by A1;
hence  ( x in dom (tan (#) tan) & x - h in dom (tan (#) tan) ) by VALUED_1:def_4; ::_thesis: verum
end;
 ( x in (dom (tan (#) tan)) /\ (dom cos) & x - h in (dom (tan (#) tan)) /\ (dom cos) ) by A2, SIN_COS:24, XBOOLE_0:def_4;
hence  ( x in dom ((tan (#) tan) (#) cos) & x - h in dom ((tan (#) tan) (#) cos) ) by VALUED_1:def_4; ::_thesis: verum
end;
then (bD (((tan (#) tan) (#) cos),h)) . x = (((tan (#) tan) (#) cos) . x) - (((tan (#) tan) (#) cos) . (x - h)) by DIFF_1:38
.= (((tan (#) tan) . x) * (cos . x)) - (((tan (#) tan) (#) cos) . (x - h)) by VALUED_1:5
.= (((tan . x) * (tan . x)) * (cos . x)) - (((tan (#) tan) (#) cos) . (x - h)) by VALUED_1:5
.= (((tan . x) * (tan . x)) * (cos . x)) - (((tan (#) tan) . (x - h)) * (cos . (x - h))) by VALUED_1:5
.= (((tan . x) * (tan . x)) * (cos . x)) - (((tan . (x - h)) * (tan . (x - h))) * (cos . (x - h))) by VALUED_1:5
.= ((((sin . x) * ((cos . x) ")) * (tan . x)) * (cos . x)) - (((tan . (x - h)) * (tan . (x - h))) * (cos . (x - h))) by A1, RFUNCT_1:def_1
.= ((((sin . x) * ((cos . x) ")) * (tan . x)) * (cos . x)) - ((((sin . (x - h)) * ((cos . (x - h)) ")) * (tan . (x - h))) * (cos . (x - h))) by A1, RFUNCT_1:def_1
.= (((sin . x) * (tan . x)) * ((cos . x) * (1 / (cos . x)))) - (((sin . (x - h)) * (tan . (x - h))) * ((cos . (x - h)) * (1 / (cos . (x - h)))))
.= (((sin . x) * (tan . x)) * 1) - (((sin . (x - h)) * (tan . (x - h))) * ((cos . (x - h)) * (1 / (cos . (x - h))))) by A1, FDIFF_8:1, XCMPLX_1:106
.= (((sin . x) * (tan . x)) * 1) - (((sin . (x - h)) * (tan . (x - h))) * 1) by A1, FDIFF_8:1, XCMPLX_1:106
.= ((tan (#) sin) . x) - ((tan . (x - h)) * (sin . (x - h))) by VALUED_1:5
.= ((tan (#) sin) . x) - ((tan (#) sin) . (x - h)) by VALUED_1:5 ;
hence  (bD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . x) - ((tan (#) sin) . (x - h)) ; ::_thesis: verum
end;

theorem :: DIFF_4:25
for x, h being Real st x + (h / 2) in dom tan & x - (h / 2) in dom tan holds
(cD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + (h / 2))) - ((tan (#) sin) . (x - (h / 2)))
proof
let x, h be Real; ::_thesis: ( x + (h / 2) in dom tan & x - (h / 2) in dom tan implies (cD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + (h / 2))) - ((tan (#) sin) . (x - (h / 2))) )
set f = (tan (#) tan) (#) cos;
assume A1: ( x + (h / 2) in dom tan & x - (h / 2) in dom tan ) ; ::_thesis: (cD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + (h / 2))) - ((tan (#) sin) . (x - (h / 2)))
 ( x + (h / 2) in dom ((tan (#) tan) (#) cos) & x - (h / 2) in dom ((tan (#) tan) (#) cos) )
proof
set f1 = tan (#) tan;
set f2 = cos ;
A2: ( x + (h / 2) in dom (tan (#) tan) & x - (h / 2) in dom (tan (#) tan) )
proof
 ( x + (h / 2) in (dom tan) /\ (dom tan) & x - (h / 2) in (dom tan) /\ (dom tan) ) by A1;
hence  ( x + (h / 2) in dom (tan (#) tan) & x - (h / 2) in dom (tan (#) tan) ) by VALUED_1:def_4; ::_thesis: verum
end;
 ( x + (h / 2) in (dom (tan (#) tan)) /\ (dom cos) & x - (h / 2) in (dom (tan (#) tan)) /\ (dom cos) ) by A2, SIN_COS:24, XBOOLE_0:def_4;
hence  ( x + (h / 2) in dom ((tan (#) tan) (#) cos) & x - (h / 2) in dom ((tan (#) tan) (#) cos) ) by VALUED_1:def_4; ::_thesis: verum
end;
then (cD (((tan (#) tan) (#) cos),h)) . x = (((tan (#) tan) (#) cos) . (x + (h / 2))) - (((tan (#) tan) (#) cos) . (x - (h / 2))) by DIFF_1:39
.= (((tan (#) tan) . (x + (h / 2))) * (cos . (x + (h / 2)))) - (((tan (#) tan) (#) cos) . (x - (h / 2))) by VALUED_1:5
.= (((tan . (x + (h / 2))) * (tan . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((tan (#) tan) (#) cos) . (x - (h / 2))) by VALUED_1:5
.= (((tan . (x + (h / 2))) * (tan . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((tan (#) tan) . (x - (h / 2))) * (cos . (x - (h / 2)))) by VALUED_1:5
.= (((tan . (x + (h / 2))) * (tan . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((tan . (x - (h / 2))) * (tan . (x - (h / 2)))) * (cos . (x - (h / 2)))) by VALUED_1:5
.= ((((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) ")) * (tan . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((tan . (x - (h / 2))) * (tan . (x - (h / 2)))) * (cos . (x - (h / 2)))) by A1, RFUNCT_1:def_1
.= ((((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) ")) * (tan . (x + (h / 2)))) * (cos . (x + (h / 2)))) - ((((sin . (x - (h / 2))) * ((cos . (x - (h / 2))) ")) * (tan . (x - (h / 2)))) * (cos . (x - (h / 2)))) by A1, RFUNCT_1:def_1
.= (((sin . (x + (h / 2))) * (tan . (x + (h / 2)))) * ((cos . (x + (h / 2))) * (1 / (cos . (x + (h / 2)))))) - (((sin . (x - (h / 2))) * (tan . (x - (h / 2)))) * ((cos . (x - (h / 2))) * (1 / (cos . (x - (h / 2))))))
.= (((sin . (x + (h / 2))) * (tan . (x + (h / 2)))) * 1) - (((sin . (x - (h / 2))) * (tan . (x - (h / 2)))) * ((cos . (x - (h / 2))) * (1 / (cos . (x - (h / 2)))))) by A1, FDIFF_8:1, XCMPLX_1:106
.= (((sin . (x + (h / 2))) * (tan . (x + (h / 2)))) * 1) - (((sin . (x - (h / 2))) * (tan . (x - (h / 2)))) * 1) by A1, FDIFF_8:1, XCMPLX_1:106
.= ((tan (#) sin) . (x + (h / 2))) - ((tan . (x - (h / 2))) * (sin . (x - (h / 2)))) by VALUED_1:5
.= ((tan (#) sin) . (x + (h / 2))) - ((tan (#) sin) . (x - (h / 2))) by VALUED_1:5 ;
hence  (cD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + (h / 2))) - ((tan (#) sin) . (x - (h / 2))) ; ::_thesis: verum
end;

theorem :: DIFF_4:26
for x0, x1 being Real st x0 in dom cot & x1 in dom cot holds
[!((cot (#) cot) (#) sin),x0,x1!] = [!(cot (#) cos),x0,x1!]
proof
let x0, x1 be Real; ::_thesis: ( x0 in dom cot & x1 in dom cot implies [!((cot (#) cot) (#) sin),x0,x1!] = [!(cot (#) cos),x0,x1!] )
assume A1: ( x0 in dom cot & x1 in dom cot ) ; ::_thesis: [!((cot (#) cot) (#) sin),x0,x1!] = [!(cot (#) cos),x0,x1!]
[!((cot (#) cot) (#) sin),x0,x1!] = ((((cot (#) cot) . x0) * (sin . x0)) - (((cot (#) cot) (#) sin) . x1)) / (x0 - x1) by VALUED_1:5
.= ((((cot . x0) * (cot . x0)) * (sin . x0)) - (((cot (#) cot) (#) sin) . x1)) / (x0 - x1) by VALUED_1:5
.= ((((cot . x0) * (cot . x0)) * (sin . x0)) - (((cot (#) cot) . x1) * (sin . x1))) / (x0 - x1) by VALUED_1:5
.= ((((cot . x0) * (cot . x0)) * (sin . x0)) - (((cot . x1) * (cot . x1)) * (sin . x1))) / (x0 - x1) by VALUED_1:5
.= (((((cos . x0) * ((sin . x0) ")) * (cot . x0)) * (sin . x0)) - (((cot . x1) * (cot . x1)) * (sin . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1
.= (((((cos . x0) * ((sin . x0) ")) * (cot . x0)) * (sin . x0)) - ((((cos . x1) * ((sin . x1) ")) * (cot . x1)) * (sin . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1
.= ((((cot . x0) * (cos . x0)) * ((sin . x0) * (1 / (sin . x0)))) - (((cot . x1) * (cos . x1)) * ((sin . x1) * (1 / (sin . x1))))) / (x0 - x1)
.= ((((cot . x0) * (cos . x0)) * 1) - (((cot . x1) * (cos . x1)) * ((sin . x1) * (1 / (sin . x1))))) / (x0 - x1) by A1, FDIFF_8:2, XCMPLX_1:106
.= ((((cot . x0) * (cos . x0)) * 1) - (((cot . x1) * (cos . x1)) * 1)) / (x0 - x1) by A1, FDIFF_8:2, XCMPLX_1:106
.= (((cot (#) cos) . x0) - ((cot . x1) * (cos . x1))) / (x0 - x1) by VALUED_1:5
.= [!(cot (#) cos),x0,x1!] by VALUED_1:5 ;
hence  [!((cot (#) cot) (#) sin),x0,x1!] = [!(cot (#) cos),x0,x1!] ; ::_thesis: verum
end;

theorem :: DIFF_4:27
for x, h being Real st x in dom cot & x + h in dom cot holds
(fD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . (x + h)) - ((cot (#) cos) . x)
proof
let x, h be Real; ::_thesis: ( x in dom cot & x + h in dom cot implies (fD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . (x + h)) - ((cot (#) cos) . x) )
set f = (cot (#) cot) (#) sin;
assume A1: ( x in dom cot & x + h in dom cot ) ; ::_thesis: (fD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . (x + h)) - ((cot (#) cos) . x)
 ( x in dom ((cot (#) cot) (#) sin) & x + h in dom ((cot (#) cot) (#) sin) )
proof
set f1 = cot (#) cot;
set f2 = sin ;
A2: ( x in dom (cot (#) cot) & x + h in dom (cot (#) cot) )
proof
 ( x in (dom cot) /\ (dom cot) & x + h in (dom cot) /\ (dom cot) ) by A1;
hence  ( x in dom (cot (#) cot) & x + h in dom (cot (#) cot) ) by VALUED_1:def_4; ::_thesis: verum
end;
 ( x in (dom (cot (#) cot)) /\ (dom sin) & x + h in (dom (cot (#) cot)) /\ (dom sin) ) by A2, SIN_COS:24, XBOOLE_0:def_4;
hence  ( x in dom ((cot (#) cot) (#) sin) & x + h in dom ((cot (#) cot) (#) sin) ) by VALUED_1:def_4; ::_thesis: verum
end;
then (fD (((cot (#) cot) (#) sin),h)) . x = (((cot (#) cot) (#) sin) . (x + h)) - (((cot (#) cot) (#) sin) . x) by DIFF_1:1
.= (((cot (#) cot) . (x + h)) * (sin . (x + h))) - (((cot (#) cot) (#) sin) . x) by VALUED_1:5
.= (((cot . (x + h)) * (cot . (x + h))) * (sin . (x + h))) - (((cot (#) cot) (#) sin) . x) by VALUED_1:5
.= (((cot . (x + h)) * (cot . (x + h))) * (sin . (x + h))) - (((cot (#) cot) . x) * (sin . x)) by VALUED_1:5
.= (((cot . (x + h)) * (cot . (x + h))) * (sin . (x + h))) - (((cot . x) * (cot . x)) * (sin . x)) by VALUED_1:5
.= ((((cos . (x + h)) * ((sin . (x + h)) ")) * (cot . (x + h))) * (sin . (x + h))) - (((cot . x) * (cot . x)) * (sin . x)) by A1, RFUNCT_1:def_1
.= ((((cos . (x + h)) * ((sin . (x + h)) ")) * (cot . (x + h))) * (sin . (x + h))) - ((((cos . x) * ((sin . x) ")) * (cot . x)) * (sin . x)) by A1, RFUNCT_1:def_1
.= (((cot . (x + h)) * (cos . (x + h))) * ((sin . (x + h)) * (1 / (sin . (x + h))))) - (((cot . x) * (cos . x)) * ((sin . x) * (1 / (sin . x))))
.= (((cot . (x + h)) * (cos . (x + h))) * 1) - (((cot . x) * (cos . x)) * ((sin . x) * (1 / (sin . x)))) by A1, FDIFF_8:2, XCMPLX_1:106
.= (((cot . (x + h)) * (cos . (x + h))) * 1) - (((cot . x) * (cos . x)) * 1) by A1, FDIFF_8:2, XCMPLX_1:106
.= ((cot (#) cos) . (x + h)) - ((cot . x) * (cos . x)) by VALUED_1:5
.= ((cot (#) cos) . (x + h)) - ((cot (#) cos) . x) by VALUED_1:5 ;
hence  (fD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . (x + h)) - ((cot (#) cos) . x) ; ::_thesis: verum
end;

theorem :: DIFF_4:28
for x, h being Real st x in dom cot & x - h in dom cot holds
(bD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . x) - ((cot (#) cos) . (x - h))
proof
let x, h be Real; ::_thesis: ( x in dom cot & x - h in dom cot implies (bD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . x) - ((cot (#) cos) . (x - h)) )
set f = (cot (#) cot) (#) sin;
assume A1: ( x in dom cot & x - h in dom cot ) ; ::_thesis: (bD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . x) - ((cot (#) cos) . (x - h))
 ( x in dom ((cot (#) cot) (#) sin) & x - h in dom ((cot (#) cot) (#) sin) )
proof
set f1 = cot (#) cot;
set f2 = sin ;
A2: ( x in dom (cot (#) cot) & x - h in dom (cot (#) cot) )
proof
 ( x in (dom cot) /\ (dom cot) & x - h in (dom cot) /\ (dom cot) ) by A1;
hence  ( x in dom (cot (#) cot) & x - h in dom (cot (#) cot) ) by VALUED_1:def_4; ::_thesis: verum
end;
 ( x in (dom (cot (#) cot)) /\ (dom sin) & x - h in (dom (cot (#) cot)) /\ (dom sin) ) by A2, SIN_COS:24, XBOOLE_0:def_4;
hence  ( x in dom ((cot (#) cot) (#) sin) & x - h in dom ((cot (#) cot) (#) sin) ) by VALUED_1:def_4; ::_thesis: verum
end;
then (bD (((cot (#) cot) (#) sin),h)) . x = (((cot (#) cot) (#) sin) . x) - (((cot (#) cot) (#) sin) . (x - h)) by DIFF_1:38
.= (((cot (#) cot) . x) * (sin . x)) - (((cot (#) cot) (#) sin) . (x - h)) by VALUED_1:5
.= (((cot . x) * (cot . x)) * (sin . x)) - (((cot (#) cot) (#) sin) . (x - h)) by VALUED_1:5
.= (((cot . x) * (cot . x)) * (sin . x)) - (((cot (#) cot) . (x - h)) * (sin . (x - h))) by VALUED_1:5
.= (((cot . x) * (cot . x)) * (sin . x)) - (((cot . (x - h)) * (cot . (x - h))) * (sin . (x - h))) by VALUED_1:5
.= ((((cos . x) * ((sin . x) ")) * (cot . x)) * (sin . x)) - (((cot . (x - h)) * (cot . (x - h))) * (sin . (x - h))) by A1, RFUNCT_1:def_1
.= ((((cos . x) * ((sin . x) ")) * (cot . x)) * (sin . x)) - ((((cos . (x - h)) * ((sin . (x - h)) ")) * (cot . (x - h))) * (sin . (x - h))) by A1, RFUNCT_1:def_1
.= (((cot . x) * (cos . x)) * ((sin . x) * (1 / (sin . x)))) - (((cot . (x - h)) * (cos . (x - h))) * ((sin . (x - h)) * (1 / (sin . (x - h)))))
.= (((cot . x) * (cos . x)) * 1) - (((cot . (x - h)) * (cos . (x - h))) * ((sin . (x - h)) * (1 / (sin . (x - h))))) by A1, FDIFF_8:2, XCMPLX_1:106
.= (((cot . x) * (cos . x)) * 1) - (((cot . (x - h)) * (cos . (x - h))) * 1) by A1, FDIFF_8:2, XCMPLX_1:106
.= ((cot (#) cos) . x) - ((cot . (x - h)) * (cos . (x - h))) by VALUED_1:5
.= ((cot (#) cos) . x) - ((cot (#) cos) . (x - h)) by VALUED_1:5 ;
hence  (bD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . x) - ((cot (#) cos) . (x - h)) ; ::_thesis: verum
end;

theorem :: DIFF_4:29
for x, h being Real st x + (h / 2) in dom cot & x - (h / 2) in dom cot holds
(cD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . (x + (h / 2))) - ((cot (#) cos) . (x - (h / 2)))
proof
let x, h be Real; ::_thesis: ( x + (h / 2) in dom cot & x - (h / 2) in dom cot implies (cD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . (x + (h / 2))) - ((cot (#) cos) . (x - (h / 2))) )
set f = (cot (#) cot) (#) sin;
assume A1: ( x + (h / 2) in dom cot & x - (h / 2) in dom cot ) ; ::_thesis: (cD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . (x + (h / 2))) - ((cot (#) cos) . (x - (h / 2)))
 ( x + (h / 2) in dom ((cot (#) cot) (#) sin) & x - (h / 2) in dom ((cot (#) cot) (#) sin) )
proof
set f1 = cot (#) cot;
set f2 = sin ;
A2: ( x + (h / 2) in dom (cot (#) cot) & x - (h / 2) in dom (cot (#) cot) )
proof
 ( x + (h / 2) in (dom cot) /\ (dom cot) & x - (h / 2) in (dom cot) /\ (dom cot) ) by A1;
hence  ( x + (h / 2) in dom (cot (#) cot) & x - (h / 2) in dom (cot (#) cot) ) by VALUED_1:def_4; ::_thesis: verum
end;
 ( x + (h / 2) in (dom (cot (#) cot)) /\ (dom sin) & x - (h / 2) in (dom (cot (#) cot)) /\ (dom sin) ) by A2, SIN_COS:24, XBOOLE_0:def_4;
hence  ( x + (h / 2) in dom ((cot (#) cot) (#) sin) & x - (h / 2) in dom ((cot (#) cot) (#) sin) ) by VALUED_1:def_4; ::_thesis: verum
end;
then (cD (((cot (#) cot) (#) sin),h)) . x = (((cot (#) cot) (#) sin) . (x + (h / 2))) - (((cot (#) cot) (#) sin) . (x - (h / 2))) by DIFF_1:39
.= (((cot (#) cot) . (x + (h / 2))) * (sin . (x + (h / 2)))) - (((cot (#) cot) (#) sin) . (x - (h / 2))) by VALUED_1:5
.= (((cot . (x + (h / 2))) * (cot . (x + (h / 2)))) * (sin . (x + (h / 2)))) - (((cot (#) cot) (#) sin) . (x - (h / 2))) by VALUED_1:5
.= (((cot . (x + (h / 2))) * (cot . (x + (h / 2)))) * (sin . (x + (h / 2)))) - (((cot (#) cot) . (x - (h / 2))) * (sin . (x - (h / 2)))) by VALUED_1:5
.= (((cot . (x + (h / 2))) * (cot . (x + (h / 2)))) * (sin . (x + (h / 2)))) - (((cot . (x - (h / 2))) * (cot . (x - (h / 2)))) * (sin . (x - (h / 2)))) by VALUED_1:5
.= ((((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * (cot . (x + (h / 2)))) * (sin . (x + (h / 2)))) - (((cot . (x - (h / 2))) * (cot . (x - (h / 2)))) * (sin . (x - (h / 2)))) by A1, RFUNCT_1:def_1
.= ((((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * (cot . (x + (h / 2)))) * (sin . (x + (h / 2)))) - ((((cos . (x - (h / 2))) * ((sin . (x - (h / 2))) ")) * (cot . (x - (h / 2)))) * (sin . (x - (h / 2)))) by A1, RFUNCT_1:def_1
.= (((cot . (x + (h / 2))) * (cos . (x + (h / 2)))) * ((sin . (x + (h / 2))) * (1 / (sin . (x + (h / 2)))))) - (((cot . (x - (h / 2))) * (cos . (x - (h / 2)))) * ((sin . (x - (h / 2))) * (1 / (sin . (x - (h / 2))))))
.= (((cot . (x + (h / 2))) * (cos . (x + (h / 2)))) * 1) - (((cot . (x - (h / 2))) * (cos . (x - (h / 2)))) * ((sin . (x - (h / 2))) * (1 / (sin . (x - (h / 2)))))) by A1, FDIFF_8:2, XCMPLX_1:106
.= (((cot . (x + (h / 2))) * (cos . (x + (h / 2)))) * 1) - (((cot . (x - (h / 2))) * (cos . (x - (h / 2)))) * 1) by A1, FDIFF_8:2, XCMPLX_1:106
.= ((cot (#) cos) . (x + (h / 2))) - ((cot . (x - (h / 2))) * (cos . (x - (h / 2)))) by VALUED_1:5
.= ((cot (#) cos) . (x + (h / 2))) - ((cot (#) cos) . (x - (h / 2))) by VALUED_1:5 ;
hence  (cD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . (x + (h / 2))) - ((cot (#) cos) . (x - (h / 2))) ; ::_thesis: verum
end;

theorem :: DIFF_4:30
for x0, x1 being Real st x0 > 0 & x1 > 0 holds
[!ln,x0,x1!] = (ln . (x0 / x1)) / (x0 - x1) by Th4;

theorem :: DIFF_4:31
for x, h being Real st x > 0 & x + h > 0 holds
(fD (ln,h)) . x = ln . (1 + (h / x))
proof
let x, h be Real; ::_thesis: ( x > 0 & x + h > 0 implies (fD (ln,h)) . x = ln . (1 + (h / x)) )
set f = ln ;
assume A1: ( x > 0 & x + h > 0 ) ; ::_thesis: (fD (ln,h)) . x = ln . (1 + (h / x))
A2: x in right_open_halfline 0
proof
 x in  {  g where g is Real : 0 < g  }  by A1;
hence  x in right_open_halfline 0 by XXREAL_1:230; ::_thesis: verum
end;
A3: x + h in right_open_halfline 0
proof
 x + h in  {  g where g is Real : 0 < g  }  by A1;
hence  x + h in right_open_halfline 0 by XXREAL_1:230; ::_thesis: verum
end;
(fD (ln,h)) . x = (ln . (x + h)) - (ln . x) by A2, A3, DIFF_1:1, TAYLOR_1:18
.= ln . ((x + h) / x) by A1, Th4
.= ln . ((x / x) + (h / x))
.= ln . (1 + (h / x)) by A1, XCMPLX_1:60 ;
hence  (fD (ln,h)) . x = ln . (1 + (h / x)) ; ::_thesis: verum
end;

theorem :: DIFF_4:32
for x, h being Real st x > 0 & x - h > 0 holds
(bD (ln,h)) . x = ln . (1 + (h / (x - h)))
proof
let x, h be Real; ::_thesis: ( x > 0 & x - h > 0 implies (bD (ln,h)) . x = ln . (1 + (h / (x - h))) )
set f = ln ;
assume A1: ( x > 0 & x - h > 0 ) ; ::_thesis: (bD (ln,h)) . x = ln . (1 + (h / (x - h)))
A2: x in right_open_halfline 0
proof
 x in  {  g where g is Real : 0 < g  }  by A1;
hence  x in right_open_halfline 0 by XXREAL_1:230; ::_thesis: verum
end;
A3: x - h in right_open_halfline 0
proof
 x - h in  {  g where g is Real : 0 < g  }  by A1;
hence  x - h in right_open_halfline 0 by XXREAL_1:230; ::_thesis: verum
end;
(bD (ln,h)) . x = (ln . x) - (ln . (x - h)) by A2, A3, DIFF_1:38, TAYLOR_1:18
.= ln . (x / (x - h)) by A1, Th4
.= ln . (((x - h) / (x - h)) + (h / (x - h)))
.= ln . (1 + (h / (x - h))) by A1, XCMPLX_1:60 ;
hence  (bD (ln,h)) . x = ln . (1 + (h / (x - h))) ; ::_thesis: verum
end;

theorem :: DIFF_4:33
for x, h being Real st x + (h / 2) > 0 & x - (h / 2) > 0 holds
(cD (ln,h)) . x = ln . (1 + (h / (x - (h / 2))))
proof
let x, h be Real; ::_thesis: ( x + (h / 2) > 0 & x - (h / 2) > 0 implies (cD (ln,h)) . x = ln . (1 + (h / (x - (h / 2)))) )
set f = ln ;
assume A1: ( x + (h / 2) > 0 & x - (h / 2) > 0 ) ; ::_thesis: (cD (ln,h)) . x = ln . (1 + (h / (x - (h / 2))))
A2: x + (h / 2) in right_open_halfline 0
proof
 x + (h / 2) in  {  g where g is Real : 0 < g  }  by A1;
hence  x + (h / 2) in right_open_halfline 0 by XXREAL_1:230; ::_thesis: verum
end;
A3: x - (h / 2) in right_open_halfline 0
proof
 x - (h / 2) in  {  g where g is Real : 0 < g  }  by A1;
hence  x - (h / 2) in right_open_halfline 0 by XXREAL_1:230; ::_thesis: verum
end;
(cD (ln,h)) . x = (ln . (x + (h / 2))) - (ln . (x - (h / 2))) by A2, A3, DIFF_1:39, TAYLOR_1:18
.= ln . (((x - (h / 2)) + h) / (x - (h / 2))) by A1, Th4
.= ln . (((x - (h / 2)) / (x - (h / 2))) + (h / (x - (h / 2))))
.= ln . (1 + (h / (x - (h / 2)))) by A1, XCMPLX_1:60 ;
hence  (cD (ln,h)) . x = ln . (1 + (h / (x - (h / 2)))) ; ::_thesis: verum
end;

theorem :: DIFF_4:34
for h, k being real number holds exp_R (h - k) = (exp_R h) / (exp_R k)
proof
let h, k be real number ; ::_thesis: exp_R (h - k) = (exp_R h) / (exp_R k)
exp_R (h - k) = (exp_R h) * (exp_R (- k)) by SIN_COS:50
.= (exp_R h) * (1 / (exp_R k)) by TAYLOR_1:4
.= (exp_R h) / (exp_R k) ;
hence  exp_R (h - k) = (exp_R h) / (exp_R k) ; ::_thesis: verum
end;

theorem :: DIFF_4:35
for h, x being Real
for f being Function of REAL,REAL holds (fD (f,h)) . x = ((Shift (f,h)) . x) - (f . x)
proof
let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (fD (f,h)) . x = ((Shift (f,h)) . x) - (f . x)
let f be Function of REAL,REAL; ::_thesis: (fD (f,h)) . x = ((Shift (f,h)) . x) - (f . x)
(fD (f,h)) . x = ((fdif (f,h)) . 1) . x by DIFF_3:7
.= ((Shift (f,h)) . x) - (f . x) by DIFF_1:11 ;
hence  (fD (f,h)) . x = ((Shift (f,h)) . x) - (f . x) ; ::_thesis: verum
end;

theorem :: DIFF_4:36
for h, x0, x1 being Real
for f, g being Function of REAL,REAL st ( for x being Real holds f . x = (fD (g,h)) . x ) holds
[!f,x0,x1!] = [!g,(x0 + h),(x1 + h)!] - [!g,x0,x1!]
proof
let h, x0, x1 be Real; ::_thesis: for f, g being Function of REAL,REAL st ( for x being Real holds f . x = (fD (g,h)) . x ) holds
[!f,x0,x1!] = [!g,(x0 + h),(x1 + h)!] - [!g,x0,x1!]
let f, g be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = (fD (g,h)) . x ) implies [!f,x0,x1!] = [!g,(x0 + h),(x1 + h)!] - [!g,x0,x1!] )
assume A1: for x being Real holds f . x = (fD (g,h)) . x ; ::_thesis: [!f,x0,x1!] = [!g,(x0 + h),(x1 + h)!] - [!g,x0,x1!]
[!f,x0,x1!] = (((fD (g,h)) . x0) - (f . x1)) / (x0 - x1) by A1
.= (((fD (g,h)) . x0) - ((fD (g,h)) . x1)) / (x0 - x1) by A1
.= (((g . (x0 + h)) - (g . x0)) - ((fD (g,h)) . x1)) / (x0 - x1) by DIFF_1:3
.= (((g . (x0 + h)) - (g . x0)) - ((g . (x1 + h)) - (g . x1))) / (x0 - x1) by DIFF_1:3
.= [!g,(x0 + h),(x1 + h)!] - [!g,x0,x1!] ;
hence  [!f,x0,x1!] = [!g,(x0 + h),(x1 + h)!] - [!g,x0,x1!] ; ::_thesis: verum
end;

theorem :: DIFF_4:37
for h, x being Real
for f being Function of REAL,REAL holds (fD ((fD (f,h)),h)) . x = ((fD (f,(2 * h))) . x) - (2 * ((fD (f,h)) . x))
proof
let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (fD ((fD (f,h)),h)) . x = ((fD (f,(2 * h))) . x) - (2 * ((fD (f,h)) . x))
let f be Function of REAL,REAL; ::_thesis: (fD ((fD (f,h)),h)) . x = ((fD (f,(2 * h))) . x) - (2 * ((fD (f,h)) . x))
(fD ((fD (f,h)),h)) . x = ((fD (f,h)) . (x + h)) - ((fD (f,h)) . x) by DIFF_1:3
.= ((f . ((x + h) + h)) - (f . (x + h))) - ((fD (f,h)) . x) by DIFF_1:3
.= ((f . ((x + h) + h)) - (f . (x + h))) - ((f . (x + h)) - (f . x)) by DIFF_1:3
.= ((f . (x + (2 * h))) - (f . x)) - ((2 * (f . (x + h))) - (2 * (f . x)))
.= ((fD (f,(2 * h))) . x) - (2 * ((f . (x + h)) - (f . x))) by DIFF_1:3
.= ((fD (f,(2 * h))) . x) - (2 * ((fD (f,h)) . x)) by DIFF_1:3 ;
hence  (fD ((fD (f,h)),h)) . x = ((fD (f,(2 * h))) . x) - (2 * ((fD (f,h)) . x)) ; ::_thesis: verum
end;

theorem :: DIFF_4:38
for h, x being Real
for f being Function of REAL,REAL holds (bD ((fD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x)
proof
let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (bD ((fD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x)
let f be Function of REAL,REAL; ::_thesis: (bD ((fD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x)
(bD ((fD (f,h)),h)) . x = ((fD (f,h)) . x) - ((fD (f,h)) . (x - h)) by DIFF_1:4
.= ((fD (f,h)) . x) - ((f . ((x - h) + h)) - (f . (x - h))) by DIFF_1:3
.= ((fD (f,h)) . x) - ((bD (f,h)) . x) by DIFF_1:4 ;
hence  (bD ((fD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x) ; ::_thesis: verum
end;

theorem :: DIFF_4:39
for h, x being Real
for f being Function of REAL,REAL holds (cD ((fD (f,h)),h)) . x = ((fD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . x)
proof
let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (cD ((fD (f,h)),h)) . x = ((fD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . x)
let f be Function of REAL,REAL; ::_thesis: (cD ((fD (f,h)),h)) . x = ((fD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . x)
(cD ((fD (f,h)),h)) . x = ((fD (f,h)) . (x + (h / 2))) - ((fD (f,h)) . (x - (h / 2))) by DIFF_1:5
.= ((fD (f,h)) . (x + (h / 2))) - ((f . ((x - (h / 2)) + h)) - (f . (x - (h / 2)))) by DIFF_1:3
.= ((fD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . x) by DIFF_1:5 ;
hence  (cD ((fD (f,h)),h)) . x = ((fD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . x) ; ::_thesis: verum
end;

theorem Th40: :: DIFF_4:40
for h, x being Real
for f being Function of REAL,REAL holds ((fdif (f,h)) . 1) . x = (((fdif (f,h)) . 0) . (x + h)) - (((fdif (f,h)) . 0) . x)
proof
let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds ((fdif (f,h)) . 1) . x = (((fdif (f,h)) . 0) . (x + h)) - (((fdif (f,h)) . 0) . x)
let f be Function of REAL,REAL; ::_thesis: ((fdif (f,h)) . 1) . x = (((fdif (f,h)) . 0) . (x + h)) - (((fdif (f,h)) . 0) . x)
((fdif (f,h)) . 1) . x = (fD (f,h)) . x by DIFF_3:7
.= (f . (x + h)) - (f . x) by DIFF_1:3
.= (((fdif (f,h)) . 0) . (x + h)) - (f . x) by DIFF_1:def_6
.= (((fdif (f,h)) . 0) . (x + h)) - (((fdif (f,h)) . 0) . x) by DIFF_1:def_6 ;
hence  ((fdif (f,h)) . 1) . x = (((fdif (f,h)) . 0) . (x + h)) - (((fdif (f,h)) . 0) . x) ; ::_thesis: verum
end;

theorem :: DIFF_4:41
for n being Element of NAT
for h, x being Real
for f being Function of REAL,REAL holds ((fdif (f,h)) . (n + 1)) . x = (((fdif (f,h)) . n) . (x + h)) - (((fdif (f,h)) . n) . x)
proof
let n be Element of NAT ; ::_thesis: for h, x being Real
for f being Function of REAL,REAL holds ((fdif (f,h)) . (n + 1)) . x = (((fdif (f,h)) . n) . (x + h)) - (((fdif (f,h)) . n) . x)
let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds ((fdif (f,h)) . (n + 1)) . x = (((fdif (f,h)) . n) . (x + h)) - (((fdif (f,h)) . n) . x)
let f be Function of REAL,REAL; ::_thesis: ((fdif (f,h)) . (n + 1)) . x = (((fdif (f,h)) . n) . (x + h)) - (((fdif (f,h)) . n) . x)
defpred S1[ Element of NAT ] means ((fdif (f,h)) . ($1 + 1)) . x = (((fdif (f,h)) . $1) . (x + h)) - (((fdif (f,h)) . $1) . x);
A1: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume  ((fdif (f,h)) . (i + 1)) . x = (((fdif (f,h)) . i) . (x + h)) - (((fdif (f,h)) . i) . x) ; ::_thesis: S1[i + 1]
A2: (fdif (f,h)) . (i + 1) is Function of REAL,REAL by DIFF_1:2;
((fdif (f,h)) . (i + 2)) . x = ((fdif (f,h)) . ((i + 1) + 1)) . x
.= (fD (((fdif (f,h)) . (i + 1)),h)) . x by DIFF_1:def_6
.= (((fdif (f,h)) . (i + 1)) . (x + h)) - (((fdif (f,h)) . (i + 1)) . x) by A2, DIFF_1:3 ;
hence  S1[i + 1] ; ::_thesis: verum
end;
A3: S1[ 0 ] by Th40;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1);
hence  ((fdif (f,h)) . (n + 1)) . x = (((fdif (f,h)) . n) . (x + h)) - (((fdif (f,h)) . n) . x) ; ::_thesis: verum
end;

theorem :: DIFF_4:42
for h, x being Real
for f being Function of REAL,REAL holds (bD (f,h)) . x = (f . x) - ((Shift (f,(- h))) . x)
proof
let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (bD (f,h)) . x = (f . x) - ((Shift (f,(- h))) . x)
let f be Function of REAL,REAL; ::_thesis: (bD (f,h)) . x = (f . x) - ((Shift (f,(- h))) . x)
(bD (f,h)) . x = ((bdif (f,h)) . 1) . x by DIFF_3:11
.= (f . x) - ((Shift (f,(- h))) . x) by DIFF_1:18 ;
hence  (bD (f,h)) . x = (f . x) - ((Shift (f,(- h))) . x) ; ::_thesis: verum
end;

theorem :: DIFF_4:43
for h, x0, x1 being Real
for f, g being Function of REAL,REAL st ( for x being Real holds f . x = (bD (g,h)) . x ) holds
[!f,x0,x1!] = [!g,x0,x1!] - [!g,(x0 - h),(x1 - h)!]
proof
let h, x0, x1 be Real; ::_thesis: for f, g being Function of REAL,REAL st ( for x being Real holds f . x = (bD (g,h)) . x ) holds
[!f,x0,x1!] = [!g,x0,x1!] - [!g,(x0 - h),(x1 - h)!]
let f, g be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = (bD (g,h)) . x ) implies [!f,x0,x1!] = [!g,x0,x1!] - [!g,(x0 - h),(x1 - h)!] )
assume A1: for x being Real holds f . x = (bD (g,h)) . x ; ::_thesis: [!f,x0,x1!] = [!g,x0,x1!] - [!g,(x0 - h),(x1 - h)!]
[!f,x0,x1!] = (((bD (g,h)) . x0) - (f . x1)) / (x0 - x1) by A1
.= (((bD (g,h)) . x0) - ((bD (g,h)) . x1)) / (x0 - x1) by A1
.= (((g . x0) - (g . (x0 - h))) - ((bD (g,h)) . x1)) / (x0 - x1) by DIFF_1:4
.= (((g . x0) - (g . (x0 - h))) - ((g . x1) - (g . (x1 - h)))) / (x0 - x1) by DIFF_1:4
.= [!g,x0,x1!] - [!g,(x0 - h),(x1 - h)!] ;
hence  [!f,x0,x1!] = [!g,x0,x1!] - [!g,(x0 - h),(x1 - h)!] ; ::_thesis: verum
end;

theorem :: DIFF_4:44
for h, x being Real
for f being Function of REAL,REAL holds (fD ((bD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x)
proof
let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (fD ((bD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x)
let f be Function of REAL,REAL; ::_thesis: (fD ((bD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x)
(fD ((bD (f,h)),h)) . x = ((bD (f,h)) . (x + h)) - ((bD (f,h)) . x) by DIFF_1:3
.= ((f . (x + h)) - (f . ((x + h) - h))) - ((bD (f,h)) . x) by DIFF_1:4
.= ((fD (f,h)) . x) - ((bD (f,h)) . x) by DIFF_1:3 ;
hence  (fD ((bD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x) ; ::_thesis: verum
end;

theorem :: DIFF_4:45
for h, x being Real
for f being Function of REAL,REAL holds (bD ((bD (f,h)),h)) . x = (2 * ((bD (f,h)) . x)) - ((bD (f,(2 * h))) . x)
proof
let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (bD ((bD (f,h)),h)) . x = (2 * ((bD (f,h)) . x)) - ((bD (f,(2 * h))) . x)
let f be Function of REAL,REAL; ::_thesis: (bD ((bD (f,h)),h)) . x = (2 * ((bD (f,h)) . x)) - ((bD (f,(2 * h))) . x)
(bD ((bD (f,h)),h)) . x = ((bD (f,h)) . x) - ((bD (f,h)) . (x - h)) by DIFF_1:4
.= ((f . x) - (f . (x - h))) - ((bD (f,h)) . (x - h)) by DIFF_1:4
.= ((f . x) - (f . (x - h))) - ((f . (x - h)) - (f . ((x - h) - h))) by DIFF_1:4
.= (2 * ((f . x) - (f . (x - h)))) - ((f . x) - (f . (x - (2 * h))))
.= (2 * ((bD (f,h)) . x)) - ((f . x) - (f . (x - (2 * h)))) by DIFF_1:4
.= (2 * ((bD (f,h)) . x)) - ((bD (f,(2 * h))) . x) by DIFF_1:4 ;
hence  (bD ((bD (f,h)),h)) . x = (2 * ((bD (f,h)) . x)) - ((bD (f,(2 * h))) . x) ; ::_thesis: verum
end;

theorem :: DIFF_4:46
for h, x being Real
for f being Function of REAL,REAL holds (cD ((bD (f,h)),h)) . x = ((cD (f,h)) . x) - ((bD (f,h)) . (x - (h / 2)))
proof
let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (cD ((bD (f,h)),h)) . x = ((cD (f,h)) . x) - ((bD (f,h)) . (x - (h / 2)))
let f be Function of REAL,REAL; ::_thesis: (cD ((bD (f,h)),h)) . x = ((cD (f,h)) . x) - ((bD (f,h)) . (x - (h / 2)))
(cD ((bD (f,h)),h)) . x = ((bD (f,h)) . (x + (h / 2))) - ((bD (f,h)) . (x - (h / 2))) by DIFF_1:5
.= ((f . (x + (h / 2))) - (f . ((x + (h / 2)) - h))) - ((bD (f,h)) . (x - (h / 2))) by DIFF_1:4
.= ((cD (f,h)) . x) - ((bD (f,h)) . (x - (h / 2))) by DIFF_1:5 ;
hence  (cD ((bD (f,h)),h)) . x = ((cD (f,h)) . x) - ((bD (f,h)) . (x - (h / 2))) ; ::_thesis: verum
end;

theorem Th47: :: DIFF_4:47
for h, x being Real
for f being Function of REAL,REAL holds ((bdif (f,h)) . 1) . x = (((bdif (f,h)) . 0) . x) - (((bdif (f,h)) . 0) . (x - h))
proof
let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds ((bdif (f,h)) . 1) . x = (((bdif (f,h)) . 0) . x) - (((bdif (f,h)) . 0) . (x - h))
let f be Function of REAL,REAL; ::_thesis: ((bdif (f,h)) . 1) . x = (((bdif (f,h)) . 0) . x) - (((bdif (f,h)) . 0) . (x - h))
((bdif (f,h)) . 1) . x = (bD (f,h)) . x by DIFF_3:11
.= (f . x) - (f . (x - h)) by DIFF_1:4
.= (((bdif (f,h)) . 0) . x) - (f . (x - h)) by DIFF_1:def_7
.= (((bdif (f,h)) . 0) . x) - (((bdif (f,h)) . 0) . (x - h)) by DIFF_1:def_7 ;
hence  ((bdif (f,h)) . 1) . x = (((bdif (f,h)) . 0) . x) - (((bdif (f,h)) . 0) . (x - h)) ; ::_thesis: verum
end;

theorem :: DIFF_4:48
for n being Element of NAT
for h, x being Real
for f being Function of REAL,REAL holds ((bdif (f,h)) . (n + 1)) . x = (((bdif (f,h)) . n) . x) - (((bdif (f,h)) . n) . (x - h))
proof
let n be Element of NAT ; ::_thesis: for h, x being Real
for f being Function of REAL,REAL holds ((bdif (f,h)) . (n + 1)) . x = (((bdif (f,h)) . n) . x) - (((bdif (f,h)) . n) . (x - h))
let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds ((bdif (f,h)) . (n + 1)) . x = (((bdif (f,h)) . n) . x) - (((bdif (f,h)) . n) . (x - h))
let f be Function of REAL,REAL; ::_thesis: ((bdif (f,h)) . (n + 1)) . x = (((bdif (f,h)) . n) . x) - (((bdif (f,h)) . n) . (x - h))
defpred S1[ Element of NAT ] means ((bdif (f,h)) . ($1 + 1)) . x = (((bdif (f,h)) . $1) . x) - (((bdif (f,h)) . $1) . (x - h));
A1: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume  ((bdif (f,h)) . (i + 1)) . x = (((bdif (f,h)) . i) . x) - (((bdif (f,h)) . i) . (x - h)) ; ::_thesis: S1[i + 1]
A2: (bdif (f,h)) . (i + 1) is Function of REAL,REAL by DIFF_1:12;
((bdif (f,h)) . (i + 2)) . x = ((bdif (f,h)) . ((i + 1) + 1)) . x
.= (bD (((bdif (f,h)) . (i + 1)),h)) . x by DIFF_1:def_7
.= (((bdif (f,h)) . (i + 1)) . x) - (((bdif (f,h)) . (i + 1)) . (x - h)) by A2, DIFF_1:4 ;
hence  S1[i + 1] ; ::_thesis: verum
end;
A3: S1[ 0 ] by Th47;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1);
hence  ((bdif (f,h)) . (n + 1)) . x = (((bdif (f,h)) . n) . x) - (((bdif (f,h)) . n) . (x - h)) ; ::_thesis: verum
end;

theorem :: DIFF_4:49
for h, x being Real
for f being Function of REAL,REAL holds (cD (f,h)) . x = ((Shift (f,(h / 2))) . x) - ((Shift (f,(- (h / 2)))) . x)
proof
let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (cD (f,h)) . x = ((Shift (f,(h / 2))) . x) - ((Shift (f,(- (h / 2)))) . x)
let f be Function of REAL,REAL; ::_thesis: (cD (f,h)) . x = ((Shift (f,(h / 2))) . x) - ((Shift (f,(- (h / 2)))) . x)
(cD (f,h)) . x = ((cdif (f,h)) . 1) . x by DIFF_3:16
.= ((Shift (f,(h / 2))) . x) - ((Shift (f,(- (h / 2)))) . x) by DIFF_1:25 ;
hence  (cD (f,h)) . x = ((Shift (f,(h / 2))) . x) - ((Shift (f,(- (h / 2)))) . x) ; ::_thesis: verum
end;

theorem :: DIFF_4:50
for h, x0, x1 being Real
for f, g being Function of REAL,REAL st ( for x being Real holds f . x = (cD (g,h)) . x ) holds
[!f,x0,x1!] = [!g,(x0 + (h / 2)),(x1 + (h / 2))!] - [!g,(x0 - (h / 2)),(x1 - (h / 2))!]
proof
let h, x0, x1 be Real; ::_thesis: for f, g being Function of REAL,REAL st ( for x being Real holds f . x = (cD (g,h)) . x ) holds
[!f,x0,x1!] = [!g,(x0 + (h / 2)),(x1 + (h / 2))!] - [!g,(x0 - (h / 2)),(x1 - (h / 2))!]
let f, g be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = (cD (g,h)) . x ) implies [!f,x0,x1!] = [!g,(x0 + (h / 2)),(x1 + (h / 2))!] - [!g,(x0 - (h / 2)),(x1 - (h / 2))!] )
assume A1: for x being Real holds f . x = (cD (g,h)) . x ; ::_thesis: [!f,x0,x1!] = [!g,(x0 + (h / 2)),(x1 + (h / 2))!] - [!g,(x0 - (h / 2)),(x1 - (h / 2))!]
[!f,x0,x1!] = (((cD (g,h)) . x0) - (f . x1)) / (x0 - x1) by A1
.= (((cD (g,h)) . x0) - ((cD (g,h)) . x1)) / (x0 - x1) by A1
.= (((g . (x0 + (h / 2))) - (g . (x0 - (h / 2)))) - ((cD (g,h)) . x1)) / (x0 - x1) by DIFF_1:5
.= (((g . (x0 + (h / 2))) - (g . (x0 - (h / 2)))) - ((g . (x1 + (h / 2))) - (g . (x1 - (h / 2))))) / (x0 - x1) by DIFF_1:5
.= [!g,(x0 + (h / 2)),(x1 + (h / 2))!] - [!g,(x0 - (h / 2)),(x1 - (h / 2))!] ;
hence  [!f,x0,x1!] = [!g,(x0 + (h / 2)),(x1 + (h / 2))!] - [!g,(x0 - (h / 2)),(x1 - (h / 2))!] ; ::_thesis: verum
end;

theorem :: DIFF_4:51
for h, x being Real
for f being Function of REAL,REAL holds (fD ((cD (f,h)),h)) . x = ((fD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . x)
proof
let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (fD ((cD (f,h)),h)) . x = ((fD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . x)
let f be Function of REAL,REAL; ::_thesis: (fD ((cD (f,h)),h)) . x = ((fD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . x)
(fD ((cD (f,h)),h)) . x = ((cD (f,h)) . (x + h)) - ((cD (f,h)) . x) by DIFF_1:3
.= ((f . ((x + h) + (h / 2))) - (f . ((x + h) - (h / 2)))) - ((cD (f,h)) . x) by DIFF_1:5
.= ((f . ((x + (h / 2)) + h)) - (f . (x + (h / 2)))) - ((cD (f,h)) . x)
.= ((fD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . x) by DIFF_1:3 ;
hence  (fD ((cD (f,h)),h)) . x = ((fD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . x) ; ::_thesis: verum
end;

theorem :: DIFF_4:52
for h, x being Real
for f being Function of REAL,REAL holds (bD ((cD (f,h)),h)) . x = ((cD (f,h)) . x) - ((bD (f,h)) . (x - (h / 2)))
proof
let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (bD ((cD (f,h)),h)) . x = ((cD (f,h)) . x) - ((bD (f,h)) . (x - (h / 2)))
let f be Function of REAL,REAL; ::_thesis: (bD ((cD (f,h)),h)) . x = ((cD (f,h)) . x) - ((bD (f,h)) . (x - (h / 2)))
(bD ((cD (f,h)),h)) . x = ((cD (f,h)) . x) - ((cD (f,h)) . (x - h)) by DIFF_1:4
.= ((cD (f,h)) . x) - ((f . ((x - h) + (h / 2))) - (f . ((x - h) - (h / 2)))) by DIFF_1:5
.= ((cD (f,h)) . x) - ((f . (x - (h / 2))) - (f . ((x - (h / 2)) - h)))
.= ((cD (f,h)) . x) - ((bD (f,h)) . (x - (h / 2))) by DIFF_1:4 ;
hence  (bD ((cD (f,h)),h)) . x = ((cD (f,h)) . x) - ((bD (f,h)) . (x - (h / 2))) ; ::_thesis: verum
end;

theorem :: DIFF_4:53
for h, x being Real
for f being Function of REAL,REAL holds (cD ((cD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x)
proof
let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds (cD ((cD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x)
let f be Function of REAL,REAL; ::_thesis: (cD ((cD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x)
(cD ((cD (f,h)),h)) . x = ((cD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . (x - (h / 2))) by DIFF_1:5
.= ((f . ((x + (h / 2)) + (h / 2))) - (f . ((x + (h / 2)) - (h / 2)))) - ((cD (f,h)) . (x - (h / 2))) by DIFF_1:5
.= ((f . ((x + (h / 2)) + (h / 2))) - (f . ((x + (h / 2)) - (h / 2)))) - ((f . ((x - (h / 2)) + (h / 2))) - (f . ((x - (h / 2)) - (h / 2)))) by DIFF_1:5
.= ((f . (x + h)) - (f . x)) - ((f . x) - (f . (x - h)))
.= ((fD (f,h)) . x) - ((f . x) - (f . (x - h))) by DIFF_1:3
.= ((fD (f,h)) . x) - ((bD (f,h)) . x) by DIFF_1:4 ;
hence  (cD ((cD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x) ; ::_thesis: verum
end;

theorem Th54: :: DIFF_4:54
for h, x being Real
for f being Function of REAL,REAL holds ((cdif (f,h)) . 1) . x = (((cdif (f,h)) . 0) . (x + (h / 2))) - (((cdif (f,h)) . 0) . (x - (h / 2)))
proof
let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds ((cdif (f,h)) . 1) . x = (((cdif (f,h)) . 0) . (x + (h / 2))) - (((cdif (f,h)) . 0) . (x - (h / 2)))
let f be Function of REAL,REAL; ::_thesis: ((cdif (f,h)) . 1) . x = (((cdif (f,h)) . 0) . (x + (h / 2))) - (((cdif (f,h)) . 0) . (x - (h / 2)))
((cdif (f,h)) . 1) . x = (cD (f,h)) . x by DIFF_3:16
.= (f . (x + (h / 2))) - (f . (x - (h / 2))) by DIFF_1:5
.= (((cdif (f,h)) . 0) . (x + (h / 2))) - (f . (x - (h / 2))) by DIFF_1:def_8
.= (((cdif (f,h)) . 0) . (x + (h / 2))) - (((cdif (f,h)) . 0) . (x - (h / 2))) by DIFF_1:def_8 ;
hence  ((cdif (f,h)) . 1) . x = (((cdif (f,h)) . 0) . (x + (h / 2))) - (((cdif (f,h)) . 0) . (x - (h / 2))) ; ::_thesis: verum
end;

theorem :: DIFF_4:55
for n being Element of NAT
for h, x being Real
for f being Function of REAL,REAL holds ((cdif (f,h)) . (n + 1)) . x = (((cdif (f,h)) . n) . (x + (h / 2))) - (((cdif (f,h)) . n) . (x - (h / 2)))
proof
let n be Element of NAT ; ::_thesis: for h, x being Real
for f being Function of REAL,REAL holds ((cdif (f,h)) . (n + 1)) . x = (((cdif (f,h)) . n) . (x + (h / 2))) - (((cdif (f,h)) . n) . (x - (h / 2)))
let h, x be Real; ::_thesis: for f being Function of REAL,REAL holds ((cdif (f,h)) . (n + 1)) . x = (((cdif (f,h)) . n) . (x + (h / 2))) - (((cdif (f,h)) . n) . (x - (h / 2)))
let f be Function of REAL,REAL; ::_thesis: ((cdif (f,h)) . (n + 1)) . x = (((cdif (f,h)) . n) . (x + (h / 2))) - (((cdif (f,h)) . n) . (x - (h / 2)))
defpred S1[ Element of NAT ] means ((cdif (f,h)) . ($1 + 1)) . x = (((cdif (f,h)) . $1) . (x + (h / 2))) - (((cdif (f,h)) . $1) . (x - (h / 2)));
A1: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume  ((cdif (f,h)) . (i + 1)) . x = (((cdif (f,h)) . i) . (x + (h / 2))) - (((cdif (f,h)) . i) . (x - (h / 2))) ; ::_thesis: S1[i + 1]
A2: (cdif (f,h)) . (i + 1) is Function of REAL,REAL by DIFF_1:19;
((cdif (f,h)) . (i + 2)) . x = ((cdif (f,h)) . ((i + 1) + 1)) . x
.= (cD (((cdif (f,h)) . (i + 1)),h)) . x by DIFF_1:def_8
.= (((cdif (f,h)) . (i + 1)) . (x + (h / 2))) - (((cdif (f,h)) . (i + 1)) . (x - (h / 2))) by A2, DIFF_1:5 ;
hence  S1[i + 1] ; ::_thesis: verum
end;
A3: S1[ 0 ] by Th54;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1);
hence  ((cdif (f,h)) . (n + 1)) . x = (((cdif (f,h)) . n) . (x + (h / 2))) - (((cdif (f,h)) . n) . (x - (h / 2))) ; ::_thesis: verum
end;

theorem :: DIFF_4:56
for x0, x1 being Real st x0 in dom tan & x1 in dom tan holds
[!((tan (#) tan) (#) sin),x0,x1!] = ((((sin x0) |^ 3) * ((cos x1) ^2)) - (((sin x1) |^ 3) * ((cos x0) ^2))) / ((((cos x0) ^2) * ((cos x1) ^2)) * (x0 - x1))
proof
let x0, x1 be Real; ::_thesis: ( x0 in dom tan & x1 in dom tan implies [!((tan (#) tan) (#) sin),x0,x1!] = ((((sin x0) |^ 3) * ((cos x1) ^2)) - (((sin x1) |^ 3) * ((cos x0) ^2))) / ((((cos x0) ^2) * ((cos x1) ^2)) * (x0 - x1)) )
assume A1: ( x0 in dom tan & x1 in dom tan ) ; ::_thesis: [!((tan (#) tan) (#) sin),x0,x1!] = ((((sin x0) |^ 3) * ((cos x1) ^2)) - (((sin x1) |^ 3) * ((cos x0) ^2))) / ((((cos x0) ^2) * ((cos x1) ^2)) * (x0 - x1))
A2: ( cos x0 <> 0 & cos x1 <> 0 ) by A1, FDIFF_8:1;
[!((tan (#) tan) (#) sin),x0,x1!] = ((((tan (#) tan) . x0) * (sin . x0)) - (((tan (#) tan) (#) sin) . x1)) / (x0 - x1) by VALUED_1:5
.= ((((tan . x0) * (tan . x0)) * (sin . x0)) - (((tan (#) tan) (#) sin) . x1)) / (x0 - x1) by VALUED_1:5
.= ((((tan . x0) * (tan . x0)) * (sin . x0)) - (((tan (#) tan) . x1) * (sin . x1))) / (x0 - x1) by VALUED_1:5
.= ((((tan . x0) * (tan . x0)) * (sin . x0)) - (((tan . x1) * (tan . x1)) * (sin . x1))) / (x0 - x1) by VALUED_1:5
.= (((((sin . x0) * ((cos . x0) ")) * (tan . x0)) * (sin . x0)) - (((tan . x1) * (tan . x1)) * (sin . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1
.= (((((sin . x0) * ((cos . x0) ")) * ((sin . x0) * ((cos . x0) "))) * (sin . x0)) - (((tan . x1) * (tan . x1)) * (sin . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1
.= (((((sin . x0) * ((cos . x0) ")) * ((sin . x0) * ((cos . x0) "))) * (sin . x0)) - ((((sin . x1) * ((cos . x1) ")) * (tan . x1)) * (sin . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1
.= (((((sin . x0) * ((cos . x0) ")) * ((sin . x0) * ((cos . x0) "))) * (sin . x0)) - ((((sin . x1) * ((cos . x1) ")) * ((sin . x1) * ((cos . x1) "))) * (sin . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1
.= ((((((sin . x0) * (sin . x0)) * (sin . x0)) * ((cos . x0) ")) * ((cos . x0) ")) - (((((sin . x1) * (sin . x1)) * (sin . x1)) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1)
.= (((((((sin . x0) |^ 1) * (sin . x0)) * (sin . x0)) * ((cos . x0) ")) * ((cos . x0) ")) - (((((sin . x1) * (sin . x1)) * (sin . x1)) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1) by NEWTON:5
.= ((((((sin . x0) |^ (1 + 1)) * (sin . x0)) * ((cos . x0) ")) * ((cos . x0) ")) - (((((sin . x1) * (sin . x1)) * (sin . x1)) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1) by NEWTON:6
.= (((((sin . x0) |^ (2 + 1)) * ((cos . x0) ")) * ((cos . x0) ")) - (((((sin . x1) * (sin . x1)) * (sin . x1)) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1) by NEWTON:6
.= (((((sin . x0) |^ 3) * ((cos . x0) ")) * ((cos . x0) ")) - ((((((sin . x1) |^ 1) * (sin . x1)) * (sin . x1)) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1) by NEWTON:5
.= (((((sin . x0) |^ 3) * ((cos . x0) ")) * ((cos . x0) ")) - (((((sin . x1) |^ (1 + 1)) * (sin . x1)) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1) by NEWTON:6
.= (((((sin . x0) |^ 3) * ((cos . x0) ")) * ((cos . x0) ")) - ((((sin . x1) |^ (2 + 1)) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1) by NEWTON:6
.= ((((sin . x0) |^ 3) * (((cos . x0) ") * ((cos . x0) "))) - ((((sin . x1) |^ 3) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1)
.= ((((sin . x0) |^ 3) * (((cos . x0) * (cos . x0)) ")) - (((sin . x1) |^ 3) * (((cos . x1) ") * ((cos . x1) ")))) / (x0 - x1) by XCMPLX_1:204
.= ((((sin . x0) |^ 3) / ((cos . x0) ^2)) - (((sin . x1) |^ 3) / ((cos . x1) ^2))) / (x0 - x1) by XCMPLX_1:204
.= (((((sin x0) |^ 3) * ((cos x1) ^2)) - (((sin x1) |^ 3) * ((cos x0) ^2))) / (((cos x0) ^2) * ((cos x1) ^2))) / (x0 - x1) by A2, XCMPLX_1:130
.= ((((sin x0) |^ 3) * ((cos x1) ^2)) - (((sin x1) |^ 3) * ((cos x0) ^2))) / ((((cos x0) ^2) * ((cos x1) ^2)) * (x0 - x1)) by XCMPLX_1:78 ;
hence  [!((tan (#) tan) (#) sin),x0,x1!] = ((((sin x0) |^ 3) * ((cos x1) ^2)) - (((sin x1) |^ 3) * ((cos x0) ^2))) / ((((cos x0) ^2) * ((cos x1) ^2)) * (x0 - x1)) ; ::_thesis: verum
end;

theorem :: DIFF_4:57
for x, h being Real st x in dom tan & x + h in dom tan holds
(fD (((tan (#) tan) (#) sin),h)) . x = (((sin . (x + h)) |^ 3) * (((cos . (x + h)) ") |^ 2)) - (((sin . x) |^ 3) * (((cos . x) ") |^ 2))
proof
let x, h be Real; ::_thesis: ( x in dom tan & x + h in dom tan implies (fD (((tan (#) tan) (#) sin),h)) . x = (((sin . (x + h)) |^ 3) * (((cos . (x + h)) ") |^ 2)) - (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) )
set f = (tan (#) tan) (#) sin;
assume A1: ( x in dom tan & x + h in dom tan ) ; ::_thesis: (fD (((tan (#) tan) (#) sin),h)) . x = (((sin . (x + h)) |^ 3) * (((cos . (x + h)) ") |^ 2)) - (((sin . x) |^ 3) * (((cos . x) ") |^ 2))
 ( x in dom ((tan (#) tan) (#) sin) & x + h in dom ((tan (#) tan) (#) sin) )
proof
set f1 = tan (#) tan;
set f2 = sin ;
A2: ( x in dom (tan (#) tan) & x + h in dom (tan (#) tan) )
proof
 ( x in (dom tan) /\ (dom tan) & x + h in (dom tan) /\ (dom tan) ) by A1;
hence  ( x in dom (tan (#) tan) & x + h in dom (tan (#) tan) ) by VALUED_1:def_4; ::_thesis: verum
end;
 ( x in (dom (tan (#) tan)) /\ (dom sin) & x + h in (dom (tan (#) tan)) /\ (dom sin) ) by A2, SIN_COS:24, XBOOLE_0:def_4;
hence  ( x in dom ((tan (#) tan) (#) sin) & x + h in dom ((tan (#) tan) (#) sin) ) by VALUED_1:def_4; ::_thesis: verum
end;
then (fD (((tan (#) tan) (#) sin),h)) . x = (((tan (#) tan) (#) sin) . (x + h)) - (((tan (#) tan) (#) sin) . x) by DIFF_1:1
.= (((tan (#) tan) . (x + h)) * (sin . (x + h))) - (((tan (#) tan) (#) sin) . x) by VALUED_1:5
.= (((tan (#) tan) . (x + h)) * (sin . (x + h))) - (((tan (#) tan) . x) * (sin . x)) by VALUED_1:5
.= (((tan . (x + h)) * (tan . (x + h))) * (sin . (x + h))) - (((tan (#) tan) . x) * (sin . x)) by VALUED_1:5
.= (((tan . (x + h)) * (tan . (x + h))) * (sin . (x + h))) - (((tan . x) * (tan . x)) * (sin . x)) by VALUED_1:5
.= ((((sin . (x + h)) * ((cos . (x + h)) ")) * (tan . (x + h))) * (sin . (x + h))) - (((tan . x) * (tan . x)) * (sin . x)) by A1, RFUNCT_1:def_1
.= ((((sin . (x + h)) * ((cos . (x + h)) ")) * ((sin . (x + h)) * ((cos . (x + h)) "))) * (sin . (x + h))) - (((tan . x) * (tan . x)) * (sin . x)) by A1, RFUNCT_1:def_1
.= ((((sin . (x + h)) * ((cos . (x + h)) ")) * ((sin . (x + h)) * ((cos . (x + h)) "))) * (sin . (x + h))) - ((((sin . x) * ((cos . x) ")) * (tan . x)) * (sin . x)) by A1, RFUNCT_1:def_1
.= ((((sin . (x + h)) * ((cos . (x + h)) ")) * ((sin . (x + h)) * ((cos . (x + h)) "))) * (sin . (x + h))) - ((((sin . x) * ((cos . x) ")) * ((sin . x) * ((cos . x) "))) * (sin . x)) by A1, RFUNCT_1:def_1
.= ((((sin . (x + h)) * (sin . (x + h))) * (sin . (x + h))) * (((cos . (x + h)) ") * ((cos . (x + h)) "))) - ((((sin . x) * (sin . x)) * (sin . x)) * (((cos . x) ") * ((cos . x) ")))
.= (((((sin . (x + h)) |^ 1) * (sin . (x + h))) * (sin . (x + h))) * (((cos . (x + h)) ") * ((cos . (x + h)) "))) - ((((sin . x) * (sin . x)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) by NEWTON:5
.= ((((sin . (x + h)) |^ (1 + 1)) * (sin . (x + h))) * (((cos . (x + h)) ") * ((cos . (x + h)) "))) - ((((sin . x) * (sin . x)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) by NEWTON:6
.= (((sin . (x + h)) |^ (2 + 1)) * (((cos . (x + h)) ") * ((cos . (x + h)) "))) - ((((sin . x) * (sin . x)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) by NEWTON:6
.= (((sin . (x + h)) |^ 3) * ((((cos . (x + h)) ") |^ 1) * ((cos . (x + h)) "))) - ((((sin . x) * (sin . x)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) by NEWTON:5
.= (((sin . (x + h)) |^ 3) * (((cos . (x + h)) ") |^ (1 + 1))) - ((((sin . x) * (sin . x)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) by NEWTON:6
.= (((sin . (x + h)) |^ 3) * (((cos . (x + h)) ") |^ 2)) - (((((sin . x) |^ 1) * (sin . x)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) by NEWTON:5
.= (((sin . (x + h)) |^ 3) * (((cos . (x + h)) ") |^ 2)) - ((((sin . x) |^ (1 + 1)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) by NEWTON:6
.= (((sin . (x + h)) |^ 3) * (((cos . (x + h)) ") |^ 2)) - (((sin . x) |^ (2 + 1)) * (((cos . x) ") * ((cos . x) "))) by NEWTON:6
.= (((sin . (x + h)) |^ 3) * (((cos . (x + h)) ") |^ 2)) - (((sin . x) |^ 3) * ((((cos . x) ") |^ 1) * ((cos . x) "))) by NEWTON:5
.= (((sin . (x + h)) |^ 3) * (((cos . (x + h)) ") |^ 2)) - (((sin . x) |^ 3) * (((cos . x) ") |^ (1 + 1))) by NEWTON:6
.= (((sin . (x + h)) |^ 3) * (((cos . (x + h)) ") |^ 2)) - (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) ;
hence  (fD (((tan (#) tan) (#) sin),h)) . x = (((sin . (x + h)) |^ 3) * (((cos . (x + h)) ") |^ 2)) - (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) ; ::_thesis: verum
end;

theorem :: DIFF_4:58
for x, h being Real st x in dom tan & x - h in dom tan holds
(bD (((tan (#) tan) (#) sin),h)) . x = (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ 3) * (((cos . (x - h)) ") |^ 2))
proof
let x, h be Real; ::_thesis: ( x in dom tan & x - h in dom tan implies (bD (((tan (#) tan) (#) sin),h)) . x = (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ 3) * (((cos . (x - h)) ") |^ 2)) )
set f = (tan (#) tan) (#) sin;
assume A1: ( x in dom tan & x - h in dom tan ) ; ::_thesis: (bD (((tan (#) tan) (#) sin),h)) . x = (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ 3) * (((cos . (x - h)) ") |^ 2))
 ( x in dom ((tan (#) tan) (#) sin) & x - h in dom ((tan (#) tan) (#) sin) )
proof
set f1 = tan (#) tan;
set f2 = sin ;
A2: ( x in dom (tan (#) tan) & x - h in dom (tan (#) tan) )
proof
 ( x in (dom tan) /\ (dom tan) & x - h in (dom tan) /\ (dom tan) ) by A1;
hence  ( x in dom (tan (#) tan) & x - h in dom (tan (#) tan) ) by VALUED_1:def_4; ::_thesis: verum
end;
 ( x in (dom (tan (#) tan)) /\ (dom sin) & x - h in (dom (tan (#) tan)) /\ (dom sin) ) by A2, SIN_COS:24, XBOOLE_0:def_4;
hence  ( x in dom ((tan (#) tan) (#) sin) & x - h in dom ((tan (#) tan) (#) sin) ) by VALUED_1:def_4; ::_thesis: verum
end;
then (bD (((tan (#) tan) (#) sin),h)) . x = (((tan (#) tan) (#) sin) . x) - (((tan (#) tan) (#) sin) . (x - h)) by DIFF_1:38
.= (((tan (#) tan) . x) * (sin . x)) - (((tan (#) tan) (#) sin) . (x - h)) by VALUED_1:5
.= (((tan (#) tan) . x) * (sin . x)) - (((tan (#) tan) . (x - h)) * (sin . (x - h))) by VALUED_1:5
.= (((tan . x) * (tan . x)) * (sin . x)) - (((tan (#) tan) . (x - h)) * (sin . (x - h))) by VALUED_1:5
.= (((tan . x) * (tan . x)) * (sin . x)) - (((tan . (x - h)) * (tan . (x - h))) * (sin . (x - h))) by VALUED_1:5
.= ((((sin . x) * ((cos . x) ")) * (tan . x)) * (sin . x)) - (((tan . (x - h)) * (tan . (x - h))) * (sin . (x - h))) by A1, RFUNCT_1:def_1
.= ((((sin . x) * ((cos . x) ")) * ((sin . x) * ((cos . x) "))) * (sin . x)) - (((tan . (x - h)) * (tan . (x - h))) * (sin . (x - h))) by A1, RFUNCT_1:def_1
.= ((((sin . x) * ((cos . x) ")) * ((sin . x) * ((cos . x) "))) * (sin . x)) - ((((sin . (x - h)) * ((cos . (x - h)) ")) * (tan . (x - h))) * (sin . (x - h))) by A1, RFUNCT_1:def_1
.= ((((sin . x) * ((cos . x) ")) * ((sin . x) * ((cos . x) "))) * (sin . x)) - ((((sin . (x - h)) * ((cos . (x - h)) ")) * ((sin . (x - h)) * ((cos . (x - h)) "))) * (sin . (x - h))) by A1, RFUNCT_1:def_1
.= ((((sin . x) * (sin . x)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) - ((((sin . (x - h)) * (sin . (x - h))) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) ")))
.= (((((sin . x) |^ 1) * (sin . x)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) - ((((sin . (x - h)) * (sin . (x - h))) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) "))) by NEWTON:5
.= ((((sin . x) |^ (1 + 1)) * (sin . x)) * (((cos . x) ") * ((cos . x) "))) - ((((sin . (x - h)) * (sin . (x - h))) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) "))) by NEWTON:6
.= (((sin . x) |^ (2 + 1)) * (((cos . x) ") * ((cos . x) "))) - ((((sin . (x - h)) * (sin . (x - h))) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) "))) by NEWTON:6
.= (((sin . x) |^ 3) * ((((cos . x) ") |^ 1) * ((cos . x) "))) - ((((sin . (x - h)) * (sin . (x - h))) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) "))) by NEWTON:5
.= (((sin . x) |^ 3) * (((cos . x) ") |^ (1 + 1))) - ((((sin . (x - h)) * (sin . (x - h))) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) "))) by NEWTON:6
.= (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((((sin . (x - h)) |^ 1) * (sin . (x - h))) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) "))) by NEWTON:5
.= (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - ((((sin . (x - h)) |^ (1 + 1)) * (sin . (x - h))) * (((cos . (x - h)) ") * ((cos . (x - h)) "))) by NEWTON:6
.= (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ (2 + 1)) * (((cos . (x - h)) ") * ((cos . (x - h)) "))) by NEWTON:6
.= (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ 3) * ((((cos . (x - h)) ") |^ 1) * ((cos . (x - h)) "))) by NEWTON:5
.= (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ 3) * (((cos . (x - h)) ") |^ (1 + 1))) by NEWTON:6
.= (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ 3) * (((cos . (x - h)) ") |^ 2)) ;
hence  (bD (((tan (#) tan) (#) sin),h)) . x = (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ 3) * (((cos . (x - h)) ") |^ 2)) ; ::_thesis: verum
end;

theorem :: DIFF_4:59
for x, h being Real st x + (h / 2) in dom tan & x - (h / 2) in dom tan holds
(cD (((tan (#) tan) (#) sin),h)) . x = (((sin . (x + (h / 2))) |^ 3) * (((cos . (x + (h / 2))) ") |^ 2)) - (((sin . (x - (h / 2))) |^ 3) * (((cos . (x - (h / 2))) ") |^ 2))
proof
let x, h be Real; ::_thesis: ( x + (h / 2) in dom tan & x - (h / 2) in dom tan implies (cD (((tan (#) tan) (#) sin),h)) . x = (((sin . (x + (h / 2))) |^ 3) * (((cos . (x + (h / 2))) ") |^ 2)) - (((sin . (x - (h / 2))) |^ 3) * (((cos . (x - (h / 2))) ") |^ 2)) )
set f = (tan (#) tan) (#) sin;
assume A1: ( x + (h / 2) in dom tan & x - (h / 2) in dom tan ) ; ::_thesis: (cD (((tan (#) tan) (#) sin),h)) . x = (((sin . (x + (h / 2))) |^ 3) * (((cos . (x + (h / 2))) ") |^ 2)) - (((sin . (x - (h / 2))) |^ 3) * (((cos . (x - (h / 2))) ") |^ 2))
 ( x + (h / 2) in dom ((tan (#) tan) (#) sin) & x - (h / 2) in dom ((tan (#) tan) (#) sin) )
proof
set f1 = tan (#) tan;
set f2 = sin ;
A2: ( x + (h / 2) in dom (tan (#) tan) & x - (h / 2) in dom (tan (#) tan) )
proof
 ( x + (h / 2) in (dom tan) /\ (dom tan) & x - (h / 2) in (dom tan) /\ (dom tan) ) by A1;
hence  ( x + (h / 2) in dom (tan (#) tan) & x - (h / 2) in dom (tan (#) tan) ) by VALUED_1:def_4; ::_thesis: verum
end;
 ( x + (h / 2) in (dom (tan (#) tan)) /\ (dom sin) & x - (h / 2) in (dom (tan (#) tan)) /\ (dom sin) ) by A2, SIN_COS:24, XBOOLE_0:def_4;
hence  ( x + (h / 2) in dom ((tan (#) tan) (#) sin) & x - (h / 2) in dom ((tan (#) tan) (#) sin) ) by VALUED_1:def_4; ::_thesis: verum
end;
then (cD (((tan (#) tan) (#) sin),h)) . x = (((tan (#) tan) (#) sin) . (x + (h / 2))) - (((tan (#) tan) (#) sin) . (x - (h / 2))) by DIFF_1:39
.= (((tan (#) tan) . (x + (h / 2))) * (sin . (x + (h / 2)))) - (((tan (#) tan) (#) sin) . (x - (h / 2))) by VALUED_1:5
.= (((tan (#) tan) . (x + (h / 2))) * (sin . (x + (h / 2)))) - (((tan (#) tan) . (x - (h / 2))) * (sin . (x - (h / 2)))) by VALUED_1:5
.= (((tan . (x + (h / 2))) * (tan . (x + (h / 2)))) * (sin . (x + (h / 2)))) - (((tan (#) tan) . (x - (h / 2))) * (sin . (x - (h / 2)))) by VALUED_1:5
.= (((tan . (x + (h / 2))) * (tan . (x + (h / 2)))) * (sin . (x + (h / 2)))) - (((tan . (x - (h / 2))) * (tan . (x - (h / 2)))) * (sin . (x - (h / 2)))) by VALUED_1:5
.= ((((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) ")) * (tan . (x + (h / 2)))) * (sin . (x + (h / 2)))) - (((tan . (x - (h / 2))) * (tan . (x - (h / 2)))) * (sin . (x - (h / 2)))) by A1, RFUNCT_1:def_1
.= ((((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) ")) * ((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) "))) * (sin . (x + (h / 2)))) - (((tan . (x - (h / 2))) * (tan . (x - (h / 2)))) * (sin . (x - (h / 2)))) by A1, RFUNCT_1:def_1
.= ((((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) ")) * ((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) "))) * (sin . (x + (h / 2)))) - ((((sin . (x - (h / 2))) * ((cos . (x - (h / 2))) ")) * (tan . (x - (h / 2)))) * (sin . (x - (h / 2)))) by A1, RFUNCT_1:def_1
.= ((((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) ")) * ((sin . (x + (h / 2))) * ((cos . (x + (h / 2))) "))) * (sin . (x + (h / 2)))) - ((((sin . (x - (h / 2))) * ((cos . (x - (h / 2))) ")) * ((sin . (x - (h / 2))) * ((cos . (x - (h / 2))) "))) * (sin . (x - (h / 2)))) by A1, RFUNCT_1:def_1
.= ((((sin . (x + (h / 2))) * (sin . (x + (h / 2)))) * (sin . (x + (h / 2)))) * (((cos . (x + (h / 2))) ") * ((cos . (x + (h / 2))) "))) - ((((sin . (x - (h / 2))) * (sin . (x - (h / 2)))) * (sin . (x - (h / 2)))) * (((cos . (x - (h / 2))) ") * ((cos . (x - (h / 2))) ")))
.= (((((sin . (x + (h / 2))) |^ 1) * (sin . (x + (h / 2)))) * (sin . (x + (h / 2)))) * (((cos . (x + (h / 2))) ") * ((cos . (x + (h / 2))) "))) - ((((sin . (x - (h / 2))) * (sin . (x - (h / 2)))) * (sin . (x - (h / 2)))) * (((cos . (x - (h / 2))) ") * ((cos . (x - (h / 2))) "))) by NEWTON:5
.= ((((sin . (x + (h / 2))) |^ (1 + 1)) * (sin . (x + (h / 2)))) * (((cos . (x + (h / 2))) ") * ((cos . (x + (h / 2))) "))) - ((((sin . (x - (h / 2))) * (sin . (x - (h / 2)))) * (sin . (x - (h / 2)))) * (((cos . (x - (h / 2))) ") * ((cos . (x - (h / 2))) "))) by NEWTON:6
.= (((sin . (x + (h / 2))) |^ (2 + 1)) * (((cos . (x + (h / 2))) ") * ((cos . (x + (h / 2))) "))) - ((((sin . (x - (h / 2))) * (sin . (x - (h / 2)))) * (sin . (x - (h / 2)))) * (((cos . (x - (h / 2))) ") * ((cos . (x - (h / 2))) "))) by NEWTON:6
.= (((sin . (x + (h / 2))) |^ 3) * ((((cos . (x + (h / 2))) ") |^ 1) * ((cos . (x + (h / 2))) "))) - ((((sin . (x - (h / 2))) * (sin . (x - (h / 2)))) * (sin . (x - (h / 2)))) * (((cos . (x - (h / 2))) ") * ((cos . (x - (h / 2))) "))) by NEWTON:5
.= (((sin . (x + (h / 2))) |^ 3) * (((cos . (x + (h / 2))) ") |^ (1 + 1))) - ((((sin . (x - (h / 2))) * (sin . (x - (h / 2)))) * (sin . (x - (h / 2)))) * (((cos . (x - (h / 2))) ") * ((cos . (x - (h / 2))) "))) by NEWTON:6
.= (((sin . (x + (h / 2))) |^ 3) * (((cos . (x + (h / 2))) ") |^ 2)) - (((((sin . (x - (h / 2))) |^ 1) * (sin . (x - (h / 2)))) * (sin . (x - (h / 2)))) * (((cos . (x - (h / 2))) ") * ((cos . (x - (h / 2))) "))) by NEWTON:5
.= (((sin . (x + (h / 2))) |^ 3) * (((cos . (x + (h / 2))) ") |^ 2)) - ((((sin . (x - (h / 2))) |^ (1 + 1)) * (sin . (x - (h / 2)))) * (((cos . (x - (h / 2))) ") * ((cos . (x - (h / 2))) "))) by NEWTON:6
.= (((sin . (x + (h / 2))) |^ 3) * (((cos . (x + (h / 2))) ") |^ 2)) - (((sin . (x - (h / 2))) |^ (2 + 1)) * (((cos . (x - (h / 2))) ") * ((cos . (x - (h / 2))) "))) by NEWTON:6
.= (((sin . (x + (h / 2))) |^ 3) * (((cos . (x + (h / 2))) ") |^ 2)) - (((sin . (x - (h / 2))) |^ 3) * ((((cos . (x - (h / 2))) ") |^ 1) * ((cos . (x - (h / 2))) "))) by NEWTON:5
.= (((sin . (x + (h / 2))) |^ 3) * (((cos . (x + (h / 2))) ") |^ 2)) - (((sin . (x - (h / 2))) |^ 3) * (((cos . (x - (h / 2))) ") |^ (1 + 1))) by NEWTON:6
.= (((sin . (x + (h / 2))) |^ 3) * (((cos . (x + (h / 2))) ") |^ 2)) - (((sin . (x - (h / 2))) |^ 3) * (((cos . (x - (h / 2))) ") |^ 2)) ;
hence  (cD (((tan (#) tan) (#) sin),h)) . x = (((sin . (x + (h / 2))) |^ 3) * (((cos . (x + (h / 2))) ") |^ 2)) - (((sin . (x - (h / 2))) |^ 3) * (((cos . (x - (h / 2))) ") |^ 2)) ; ::_thesis: verum
end;

theorem :: DIFF_4:60
for x0, x1 being Real st x0 in dom cot & x1 in dom cot holds
[!((cot (#) cot) (#) cos),x0,x1!] = ((((cos x0) |^ 3) * ((sin x1) ^2)) - (((cos x1) |^ 3) * ((sin x0) ^2))) / ((((sin x0) ^2) * ((sin x1) ^2)) * (x0 - x1))
proof
let x0, x1 be Real; ::_thesis: ( x0 in dom cot & x1 in dom cot implies [!((cot (#) cot) (#) cos),x0,x1!] = ((((cos x0) |^ 3) * ((sin x1) ^2)) - (((cos x1) |^ 3) * ((sin x0) ^2))) / ((((sin x0) ^2) * ((sin x1) ^2)) * (x0 - x1)) )
assume A1: ( x0 in dom cot & x1 in dom cot ) ; ::_thesis: [!((cot (#) cot) (#) cos),x0,x1!] = ((((cos x0) |^ 3) * ((sin x1) ^2)) - (((cos x1) |^ 3) * ((sin x0) ^2))) / ((((sin x0) ^2) * ((sin x1) ^2)) * (x0 - x1))
A2: ( sin x0 <> 0 & sin x1 <> 0 ) by A1, FDIFF_8:2;
[!((cot (#) cot) (#) cos),x0,x1!] = ((((cot (#) cot) . x0) * (cos . x0)) - (((cot (#) cot) (#) cos) . x1)) / (x0 - x1) by VALUED_1:5
.= ((((cot . x0) * (cot . x0)) * (cos . x0)) - (((cot (#) cot) (#) cos) . x1)) / (x0 - x1) by VALUED_1:5
.= ((((cot . x0) * (cot . x0)) * (cos . x0)) - (((cot (#) cot) . x1) * (cos . x1))) / (x0 - x1) by VALUED_1:5
.= ((((cot . x0) * (cot . x0)) * (cos . x0)) - (((cot . x1) * (cot . x1)) * (cos . x1))) / (x0 - x1) by VALUED_1:5
.= (((((cos . x0) * ((sin . x0) ")) * (cot . x0)) * (cos . x0)) - (((cot . x1) * (cot . x1)) * (cos . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1
.= (((((cos . x0) * ((sin . x0) ")) * ((cos . x0) * ((sin . x0) "))) * (cos . x0)) - (((cot . x1) * (cot . x1)) * (cos . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1
.= (((((cos . x0) * ((sin . x0) ")) * ((cos . x0) * ((sin . x0) "))) * (cos . x0)) - ((((cos . x1) * ((sin . x1) ")) * (cot . x1)) * (cos . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1
.= (((((cos . x0) * ((sin . x0) ")) * ((cos . x0) * ((sin . x0) "))) * (cos . x0)) - ((((cos . x1) * ((sin . x1) ")) * ((cos . x1) * ((sin . x1) "))) * (cos . x1))) / (x0 - x1) by A1, RFUNCT_1:def_1
.= ((((((cos . x0) * (cos . x0)) * (cos . x0)) * ((sin . x0) ")) * ((sin . x0) ")) - (((((cos . x1) * (cos . x1)) * (cos . x1)) * ((sin . x1) ")) * ((sin . x1) "))) / (x0 - x1)
.= (((((((cos . x0) |^ 1) * (cos . x0)) * (cos . x0)) * ((sin . x0) ")) * ((sin . x0) ")) - (((((cos . x1) * (cos . x1)) * (cos . x1)) * ((sin . x1) ")) * ((sin . x1) "))) / (x0 - x1) by NEWTON:5
.= ((((((cos . x0) |^ (1 + 1)) * (cos . x0)) * ((sin . x0) ")) * ((sin . x0) ")) - (((((cos . x1) * (cos . x1)) * (cos . x1)) * ((sin . x1) ")) * ((sin . x1) "))) / (x0 - x1) by NEWTON:6
.= (((((cos . x0) |^ (2 + 1)) * ((sin . x0) ")) * ((sin . x0) ")) - (((((cos . x1) * (cos . x1)) * (cos . x1)) * ((sin . x1) ")) * ((sin . x1) "))) / (x0 - x1) by NEWTON:6
.= (((((cos . x0) |^ 3) * ((sin . x0) ")) * ((sin . x0) ")) - ((((((cos . x1) |^ 1) * (cos . x1)) * (cos . x1)) * ((sin . x1) ")) * ((sin . x1) "))) / (x0 - x1) by NEWTON:5
.= (((((cos . x0) |^ 3) * ((sin . x0) ")) * ((sin . x0) ")) - (((((cos . x1) |^ (1 + 1)) * (cos . x1)) * ((sin . x1) ")) * ((sin . x1) "))) / (x0 - x1) by NEWTON:6
.= (((((cos . x0) |^ 3) * ((sin . x0) ")) * ((sin . x0) ")) - ((((cos . x1) |^ (2 + 1)) * ((sin . x1) ")) * ((sin . x1) "))) / (x0 - x1) by NEWTON:6
.= ((((cos . x0) |^ 3) * (((sin . x0) ") * ((sin . x0) "))) - ((((cos . x1) |^ 3) * ((sin . x1) ")) * ((sin . x1) "))) / (x0 - x1)
.= ((((cos . x0) |^ 3) * (((sin . x0) * (sin . x0)) ")) - (((cos . x1) |^ 3) * (((sin . x1) ") * ((sin . x1) ")))) / (x0 - x1) by XCMPLX_1:204
.= ((((cos . x0) |^ 3) / ((sin . x0) ^2)) - (((cos . x1) |^ 3) / ((sin . x1) ^2))) / (x0 - x1) by XCMPLX_1:204
.= (((((cos x0) |^ 3) * ((sin x1) ^2)) - (((cos x1) |^ 3) * ((sin x0) ^2))) / (((sin x0) ^2) * ((sin x1) ^2))) / (x0 - x1) by A2, XCMPLX_1:130
.= ((((cos x0) |^ 3) * ((sin x1) ^2)) - (((cos x1) |^ 3) * ((sin x0) ^2))) / ((((sin x0) ^2) * ((sin x1) ^2)) * (x0 - x1)) by XCMPLX_1:78 ;
hence  [!((cot (#) cot) (#) cos),x0,x1!] = ((((cos x0) |^ 3) * ((sin x1) ^2)) - (((cos x1) |^ 3) * ((sin x0) ^2))) / ((((sin x0) ^2) * ((sin x1) ^2)) * (x0 - x1)) ; ::_thesis: verum
end;

theorem :: DIFF_4:61
for x, h being Real st x in dom cot & x + h in dom cot holds
(fD (((cot (#) cot) (#) cos),h)) . x = (((cos . (x + h)) |^ 3) * (((sin . (x + h)) ") |^ 2)) - (((cos . x) |^ 3) * (((sin . x) ") |^ 2))
proof
let x, h be Real; ::_thesis: ( x in dom cot & x + h in dom cot implies (fD (((cot (#) cot) (#) cos),h)) . x = (((cos . (x + h)) |^ 3) * (((sin . (x + h)) ") |^ 2)) - (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) )
set f = (cot (#) cot) (#) cos;
assume A1: ( x in dom cot & x + h in dom cot ) ; ::_thesis: (fD (((cot (#) cot) (#) cos),h)) . x = (((cos . (x + h)) |^ 3) * (((sin . (x + h)) ") |^ 2)) - (((cos . x) |^ 3) * (((sin . x) ") |^ 2))
 ( x in dom ((cot (#) cot) (#) cos) & x + h in dom ((cot (#) cot) (#) cos) )
proof
set f1 = cot (#) cot;
set f2 = cos ;
A2: ( x in dom (cot (#) cot) & x + h in dom (cot (#) cot) )
proof
 ( x in (dom cot) /\ (dom cot) & x + h in (dom cot) /\ (dom cot) ) by A1;
hence  ( x in dom (cot (#) cot) & x + h in dom (cot (#) cot) ) by VALUED_1:def_4; ::_thesis: verum
end;
 ( x in (dom (cot (#) cot)) /\ (dom cos) & x + h in (dom (cot (#) cot)) /\ (dom cos) ) by A2, SIN_COS:24, XBOOLE_0:def_4;
hence  ( x in dom ((cot (#) cot) (#) cos) & x + h in dom ((cot (#) cot) (#) cos) ) by VALUED_1:def_4; ::_thesis: verum
end;
then (fD (((cot (#) cot) (#) cos),h)) . x = (((cot (#) cot) (#) cos) . (x + h)) - (((cot (#) cot) (#) cos) . x) by DIFF_1:1
.= (((cot (#) cot) . (x + h)) * (cos . (x + h))) - (((cot (#) cot) (#) cos) . x) by VALUED_1:5
.= (((cot (#) cot) . (x + h)) * (cos . (x + h))) - (((cot (#) cot) . x) * (cos . x)) by VALUED_1:5
.= (((cot . (x + h)) * (cot . (x + h))) * (cos . (x + h))) - (((cot (#) cot) . x) * (cos . x)) by VALUED_1:5
.= (((cot . (x + h)) * (cot . (x + h))) * (cos . (x + h))) - (((cot . x) * (cot . x)) * (cos . x)) by VALUED_1:5
.= ((((cos . (x + h)) * ((sin . (x + h)) ")) * (cot . (x + h))) * (cos . (x + h))) - (((cot . x) * (cot . x)) * (cos . x)) by A1, RFUNCT_1:def_1
.= ((((cos . (x + h)) * ((sin . (x + h)) ")) * ((cos . (x + h)) * ((sin . (x + h)) "))) * (cos . (x + h))) - (((cot . x) * (cot . x)) * (cos . x)) by A1, RFUNCT_1:def_1
.= ((((cos . (x + h)) * ((sin . (x + h)) ")) * ((cos . (x + h)) * ((sin . (x + h)) "))) * (cos . (x + h))) - ((((cos . x) * ((sin . x) ")) * (cot . x)) * (cos . x)) by A1, RFUNCT_1:def_1
.= ((((cos . (x + h)) * ((sin . (x + h)) ")) * ((cos . (x + h)) * ((sin . (x + h)) "))) * (cos . (x + h))) - ((((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) * (cos . x)) by A1, RFUNCT_1:def_1
.= ((((cos . (x + h)) * (cos . (x + h))) * (cos . (x + h))) * (((sin . (x + h)) ") * ((sin . (x + h)) "))) - ((((cos . x) * (cos . x)) * (cos . x)) * (((sin . x) ") * ((sin . x) ")))
.= (((((cos . (x + h)) |^ 1) * (cos . (x + h))) * (cos . (x + h))) * (((sin . (x + h)) ") * ((sin . (x + h)) "))) - ((((cos . x) * (cos . x)) * (cos . x)) * (((sin . x) ") * ((sin . x) "))) by NEWTON:5
.= ((((cos . (x + h)) |^ (1 + 1)) * (cos . (x + h))) * (((sin . (x + h)) ") * ((sin . (x + h)) "))) - ((((cos . x) * (cos . x)) * (cos . x)) * (((sin . x) ") * ((sin . x) "))) by NEWTON:6
.= (((cos . (x + h)) |^ (2 + 1)) * (((sin . (x + h)) ") * ((sin . (x + h)) "))) - ((((cos . x) * (cos . x)) * (cos . x)) * (((sin . x) ") * ((sin . x) "))) by NEWTON:6
.= (((cos . (x + h)) |^ 3) * ((((sin . (x + h)) ") |^ 1) * ((sin . (x + h)) "))) - ((((cos . x) * (cos . x)) * (cos . x)) * (((sin . x) ") * ((sin . x) "))) by NEWTON:5
.= (((cos . (x + h)) |^ 3) * (((sin . (x + h)) ") |^ (1 + 1))) - ((((cos . x) * (cos . x)) * (cos . x)) * (((sin . x) ") * ((sin . x) "))) by NEWTON:6
.= (((cos . (x + h)) |^ 3) * (((sin . (x + h)) ") |^ 2)) - (((((cos . x) |^ 1) * (cos . x)) * (cos . x)) * (((sin . x) ") * ((sin . x) "))) by NEWTON:5
.= (((cos . (x + h)) |^ 3) * (((sin . (x + h)) ") |^ 2)) - ((((cos . x) |^ (1 + 1)) * (cos . x)) * (((sin . x) ") * ((sin . x) "))) by NEWTON:6
.= (((cos . (x + h)) |^ 3) * (((sin . (x + h)) ") |^ 2)) - (((cos . x) |^ (2 + 1)) * (((sin . x) ") * ((sin . x) "))) by NEWTON:6
.= (((cos . (x + h)) |^ 3) * (((sin . (x + h)) ") |^ 2)) - (((cos . x) |^ 3) * ((((sin . x) ") |^ 1) * ((sin . x) "))) by NEWTON:5
.= (((cos . (x + h)) |^ 3) * (((sin . (x + h)) ") |^ 2)) - (((cos . x) |^ 3) * (((sin . x) ") |^ (1 + 1))) by NEWTON:6
.= (((cos . (x + h)) |^ 3) * (((sin . (x + h)) ") |^ 2)) - (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) ;
hence  (fD (((cot (#) cot) (#) cos),h)) . x = (((cos . (x + h)) |^ 3) * (((sin . (x + h)) ") |^ 2)) - (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) ; ::_thesis: verum
end;

theorem :: DIFF_4:62
for x, h being Real st x in dom cot & x - h in dom cot holds
(bD (((cot (#) cot) (#) cos),h)) . x = (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) - (((cos . (x - h)) |^ 3) * (((sin . (x - h)) ") |^ 2))
proof
let x, h be Real; ::_thesis: ( x in dom cot & x - h in dom cot implies (bD (((cot (#) cot) (#) cos),h)) . x = (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) - (((cos . (x - h)) |^ 3) * (((sin . (x - h)) ") |^ 2)) )
set f = (cot (#) cot) (#) cos;
assume A1: ( x in dom cot & x - h in dom cot ) ; ::_thesis: (bD (((cot (#) cot) (#) cos),h)) . x = (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) - (((cos . (x - h)) |^ 3) * (((sin . (x - h)) ") |^ 2))
 ( x in dom ((cot (#) cot) (#) cos) & x - h in dom ((cot (#) cot) (#) cos) )
proof
set f1 = cot (#) cot;
set f2 = cos ;
A2: ( x in dom (cot (#) cot) & x - h in dom (cot (#) cot) )
proof
 ( x in (dom cot) /\ (dom cot) & x - h in (dom cot) /\ (dom cot) ) by A1;
hence  ( x in dom (cot (#) cot) & x - h in dom (cot (#) cot) ) by VALUED_1:def_4; ::_thesis: verum
end;
 ( x in (dom (cot (#) cot)) /\ (dom cos) & x - h in (dom (cot (#) cot)) /\ (dom cos) ) by A2, SIN_COS:24, XBOOLE_0:def_4;
hence  ( x in dom ((cot (#) cot) (#) cos) & x - h in dom ((cot (#) cot) (#) cos) ) by VALUED_1:def_4; ::_thesis: verum
end;
then (bD (((cot (#) cot) (#) cos),h)) . x = (((cot (#) cot) (#) cos) . x) - (((cot (#) cot) (#) cos) . (x - h)) by DIFF_1:38
.= (((cot (#) cot) . x) * (cos . x)) - (((cot (#) cot) (#) cos) . (x - h)) by VALUED_1:5
.= (((cot (#) cot) . x) * (cos . x)) - (((cot (#) cot) . (x - h)) * (cos . (x - h))) by VALUED_1:5
.= (((cot . x) * (cot . x)) * (cos . x)) - (((cot (#) cot) . (x - h)) * (cos . (x - h))) by VALUED_1:5
.= (((cot . x) * (cot . x)) * (cos . x)) - (((cot . (x - h)) * (cot . (x - h))) * (cos . (x - h))) by VALUED_1:5
.= ((((cos . x) * ((sin . x) ")) * (cot . x)) * (cos . x)) - (((cot . (x - h)) * (cot . (x - h))) * (cos . (x - h))) by A1, RFUNCT_1:def_1
.= ((((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) * (cos . x)) - (((cot . (x - h)) * (cot . (x - h))) * (cos . (x - h))) by A1, RFUNCT_1:def_1
.= ((((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) * (cos . x)) - ((((cos . (x - h)) * ((sin . (x - h)) ")) * (cot . (x - h))) * (cos . (x - h))) by A1, RFUNCT_1:def_1
.= ((((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) * (cos . x)) - ((((cos . (x - h)) * ((sin . (x - h)) ")) * ((cos . (x - h)) * ((sin . (x - h)) "))) * (cos . (x - h))) by A1, RFUNCT_1:def_1
.= ((((cos . x) * (cos . x)) * (cos . x)) * (((sin . x) ") * ((sin . x) "))) - ((((cos . (x - h)) * (cos . (x - h))) * (cos . (x - h))) * (((sin . (x - h)) ") * ((sin . (x - h)) ")))
.= (((((cos . x) |^ 1) * (cos . x)) * (cos . x)) * (((sin . x) ") * ((sin . x) "))) - ((((cos . (x - h)) * (cos . (x - h))) * (cos . (x - h))) * (((sin . (x - h)) ") * ((sin . (x - h)) "))) by NEWTON:5
.= ((((cos . x) |^ (1 + 1)) * (cos . x)) * (((sin . x) ") * ((sin . x) "))) - ((((cos . (x - h)) * (cos . (x - h))) * (cos . (x - h))) * (((sin . (x - h)) ") * ((sin . (x - h)) "))) by NEWTON:6
.= (((cos . x) |^ (2 + 1)) * (((sin . x) ") * ((sin . x) "))) - ((((cos . (x - h)) * (cos . (x - h))) * (cos . (x - h))) * (((sin . (x - h)) ") * ((sin . (x - h)) "))) by NEWTON:6
.= (((cos . x) |^ 3) * ((((sin . x) ") |^ 1) * ((sin . x) "))) - ((((cos . (x - h)) * (cos . (x - h))) * (cos . (x - h))) * (((sin . (x - h)) ") * ((sin . (x - h)) "))) by NEWTON:5
.= (((cos . x) |^ 3) * (((sin . x) ") |^ (1 + 1))) - ((((cos . (x - h)) * (cos . (x - h))) * (cos . (x - h))) * (((sin . (x - h)) ") * ((sin . (x - h)) "))) by NEWTON:6
.= (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) - (((((cos . (x - h)) |^ 1) * (cos . (x - h))) * (cos . (x - h))) * (((sin . (x - h)) ") * ((sin . (x - h)) "))) by NEWTON:5
.= (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) - ((((cos . (x - h)) |^ (1 + 1)) * (cos . (x - h))) * (((sin . (x - h)) ") * ((sin . (x - h)) "))) by NEWTON:6
.= (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) - (((cos . (x - h)) |^ (2 + 1)) * (((sin . (x - h)) ") * ((sin . (x - h)) "))) by NEWTON:6
.= (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) - (((cos . (x - h)) |^ 3) * ((((sin . (x - h)) ") |^ 1) * ((sin . (x - h)) "))) by NEWTON:5
.= (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) - (((cos . (x - h)) |^ 3) * (((sin . (x - h)) ") |^ (1 + 1))) by NEWTON:6
.= (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) - (((cos . (x - h)) |^ 3) * (((sin . (x - h)) ") |^ 2)) ;
hence  (bD (((cot (#) cot) (#) cos),h)) . x = (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) - (((cos . (x - h)) |^ 3) * (((sin . (x - h)) ") |^ 2)) ; ::_thesis: verum
end;

theorem :: DIFF_4:63
for x, h being Real st x + (h / 2) in dom cot & x - (h / 2) in dom cot holds
(cD (((cot (#) cot) (#) cos),h)) . x = (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((cos . (x - (h / 2))) |^ 3) * (((sin . (x - (h / 2))) ") |^ 2))
proof
let x, h be Real; ::_thesis: ( x + (h / 2) in dom cot & x - (h / 2) in dom cot implies (cD (((cot (#) cot) (#) cos),h)) . x = (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((cos . (x - (h / 2))) |^ 3) * (((sin . (x - (h / 2))) ") |^ 2)) )
set f = (cot (#) cot) (#) cos;
assume A1: ( x + (h / 2) in dom cot & x - (h / 2) in dom cot ) ; ::_thesis: (cD (((cot (#) cot) (#) cos),h)) . x = (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((cos . (x - (h / 2))) |^ 3) * (((sin . (x - (h / 2))) ") |^ 2))
 ( x + (h / 2) in dom ((cot (#) cot) (#) cos) & x - (h / 2) in dom ((cot (#) cot) (#) cos) )
proof
set f1 = cot (#) cot;
set f2 = cos ;
A2: ( x + (h / 2) in dom (cot (#) cot) & x - (h / 2) in dom (cot (#) cot) )
proof
 ( x + (h / 2) in (dom cot) /\ (dom cot) & x - (h / 2) in (dom cot) /\ (dom cot) ) by A1;
hence  ( x + (h / 2) in dom (cot (#) cot) & x - (h / 2) in dom (cot (#) cot) ) by VALUED_1:def_4; ::_thesis: verum
end;
 ( x + (h / 2) in (dom (cot (#) cot)) /\ (dom cos) & x - (h / 2) in (dom (cot (#) cot)) /\ (dom cos) ) by A2, SIN_COS:24, XBOOLE_0:def_4;
hence  ( x + (h / 2) in dom ((cot (#) cot) (#) cos) & x - (h / 2) in dom ((cot (#) cot) (#) cos) ) by VALUED_1:def_4; ::_thesis: verum
end;
then (cD (((cot (#) cot) (#) cos),h)) . x = (((cot (#) cot) (#) cos) . (x + (h / 2))) - (((cot (#) cot) (#) cos) . (x - (h / 2))) by DIFF_1:39
.= (((cot (#) cot) . (x + (h / 2))) * (cos . (x + (h / 2)))) - (((cot (#) cot) (#) cos) . (x - (h / 2))) by VALUED_1:5
.= (((cot (#) cot) . (x + (h / 2))) * (cos . (x + (h / 2)))) - (((cot (#) cot) . (x - (h / 2))) * (cos . (x - (h / 2)))) by VALUED_1:5
.= (((cot . (x + (h / 2))) * (cot . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((cot (#) cot) . (x - (h / 2))) * (cos . (x - (h / 2)))) by VALUED_1:5
.= (((cot . (x + (h / 2))) * (cot . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((cot . (x - (h / 2))) * (cot . (x - (h / 2)))) * (cos . (x - (h / 2)))) by VALUED_1:5
.= ((((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * (cot . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((cot . (x - (h / 2))) * (cot . (x - (h / 2)))) * (cos . (x - (h / 2)))) by A1, RFUNCT_1:def_1
.= ((((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * ((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) "))) * (cos . (x + (h / 2)))) - (((cot . (x - (h / 2))) * (cot . (x - (h / 2)))) * (cos . (x - (h / 2)))) by A1, RFUNCT_1:def_1
.= ((((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * ((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) "))) * (cos . (x + (h / 2)))) - ((((cos . (x - (h / 2))) * ((sin . (x - (h / 2))) ")) * (cot . (x - (h / 2)))) * (cos . (x - (h / 2)))) by A1, RFUNCT_1:def_1
.= ((((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * ((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) "))) * (cos . (x + (h / 2)))) - ((((cos . (x - (h / 2))) * ((sin . (x - (h / 2))) ")) * ((cos . (x - (h / 2))) * ((sin . (x - (h / 2))) "))) * (cos . (x - (h / 2)))) by A1, RFUNCT_1:def_1
.= ((((cos . (x + (h / 2))) * (cos . (x + (h / 2)))) * (cos . (x + (h / 2)))) * (((sin . (x + (h / 2))) ") * ((sin . (x + (h / 2))) "))) - ((((cos . (x - (h / 2))) * (cos . (x - (h / 2)))) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) ")))
.= (((((cos . (x + (h / 2))) |^ 1) * (cos . (x + (h / 2)))) * (cos . (x + (h / 2)))) * (((sin . (x + (h / 2))) ") * ((sin . (x + (h / 2))) "))) - ((((cos . (x - (h / 2))) * (cos . (x - (h / 2)))) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) "))) by NEWTON:5
.= ((((cos . (x + (h / 2))) |^ (1 + 1)) * (cos . (x + (h / 2)))) * (((sin . (x + (h / 2))) ") * ((sin . (x + (h / 2))) "))) - ((((cos . (x - (h / 2))) * (cos . (x - (h / 2)))) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) "))) by NEWTON:6
.= (((cos . (x + (h / 2))) |^ (2 + 1)) * (((sin . (x + (h / 2))) ") * ((sin . (x + (h / 2))) "))) - ((((cos . (x - (h / 2))) * (cos . (x - (h / 2)))) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) "))) by NEWTON:6
.= (((cos . (x + (h / 2))) |^ 3) * ((((sin . (x + (h / 2))) ") |^ 1) * ((sin . (x + (h / 2))) "))) - ((((cos . (x - (h / 2))) * (cos . (x - (h / 2)))) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) "))) by NEWTON:5
.= (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ (1 + 1))) - ((((cos . (x - (h / 2))) * (cos . (x - (h / 2)))) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) "))) by NEWTON:6
.= (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((((cos . (x - (h / 2))) |^ 1) * (cos . (x - (h / 2)))) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) "))) by NEWTON:5
.= (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - ((((cos . (x - (h / 2))) |^ (1 + 1)) * (cos . (x - (h / 2)))) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) "))) by NEWTON:6
.= (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((cos . (x - (h / 2))) |^ (2 + 1)) * (((sin . (x - (h / 2))) ") * ((sin . (x - (h / 2))) "))) by NEWTON:6
.= (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((cos . (x - (h / 2))) |^ 3) * ((((sin . (x - (h / 2))) ") |^ 1) * ((sin . (x - (h / 2))) "))) by NEWTON:5
.= (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((cos . (x - (h / 2))) |^ 3) * (((sin . (x - (h / 2))) ") |^ (1 + 1))) by NEWTON:6
.= (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((cos . (x - (h / 2))) |^ 3) * (((sin . (x - (h / 2))) ") |^ 2)) ;
hence  (cD (((cot (#) cot) (#) cos),h)) . x = (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((cos . (x - (h / 2))) |^ 3) * (((sin . (x - (h / 2))) ") |^ 2)) ; ::_thesis: verum
end;