:: DIFF_2 semantic presentation

begin


theorem Th1: :: DIFF_2:1
for x, h being Real
for f being Function of REAL,REAL holds [!f,x,(x + h)!] = (((fdif (f,h)) . 1) . x) / h
proof
let x, h be Real; ::_thesis: for f being Function of REAL,REAL holds [!f,x,(x + h)!] = (((fdif (f,h)) . 1) . x) / h
let f be Function of REAL,REAL; ::_thesis: [!f,x,(x + h)!] = (((fdif (f,h)) . 1) . x) / h
[!f,x,(x + h)!] = [!f,(x + h),x!] by DIFF_1:29
.= ((fD (f,h)) . x) / h by DIFF_1:3
.= ((fD (((fdif (f,h)) . 0),h)) . x) / h by DIFF_1:def_6
.= (((fdif (f,h)) . (0 + 1)) . x) / h by DIFF_1:def_6 ;
hence  [!f,x,(x + h)!] = (((fdif (f,h)) . 1) . x) / h ; ::_thesis: verum
end;

theorem :: DIFF_2:2
for h, x being Real
for f being Function of REAL,REAL st h <> 0 holds
[!f,x,(x + h),(x + (2 * h))!] = (((fdif (f,h)) . 2) . x) / (2 * (h ^2))
proof
let h, x be Real; ::_thesis: for f being Function of REAL,REAL st h <> 0 holds
[!f,x,(x + h),(x + (2 * h))!] = (((fdif (f,h)) . 2) . x) / (2 * (h ^2))
let f be Function of REAL,REAL; ::_thesis: ( h <> 0 implies [!f,x,(x + h),(x + (2 * h))!] = (((fdif (f,h)) . 2) . x) / (2 * (h ^2)) )
A1: (fdif (f,h)) . 1 is Function of REAL,REAL by DIFF_1:2;
assume A2: h <> 0 ; ::_thesis: [!f,x,(x + h),(x + (2 * h))!] = (((fdif (f,h)) . 2) . x) / (2 * (h ^2))
then A3: x + h <> x + (2 * h) ;
 ( x <> x + h & x <> x + (2 * h) ) by A2;
then  x,x + h,x + (2 * h) are_mutually_different by A3, ZFMISC_1:def_5;
then [!f,x,(x + h),(x + (2 * h))!] = [!f,(x + (2 * h)),(x + h),x!] by DIFF_1:34
.= ([!f,(x + h),(x + (2 * h))!] - [!f,(x + h),x!]) / ((x + (2 * h)) - x) by DIFF_1:29
.= ([!f,(x + h),((x + h) + h)!] - [!f,x,(x + h)!]) / ((x + (2 * h)) - x) by DIFF_1:29
.= (((((fdif (f,h)) . 1) . (x + h)) / h) - [!f,x,(x + h)!]) / ((x + (2 * h)) - x) by Th1
.= (((((fdif (f,h)) . 1) . (x + h)) / h) - ((((fdif (f,h)) . 1) . x) / h)) / ((x + (2 * h)) - x) by Th1
.= (((((fdif (f,h)) . 1) . (x + h)) - (((fdif (f,h)) . 1) . x)) / h) / ((x + (2 * h)) - x) by XCMPLX_1:120
.= (((fD (((fdif (f,h)) . 1),h)) . x) / h) / (2 * h) by A1, DIFF_1:3
.= ((((fdif (f,h)) . (1 + 1)) . x) / h) / (2 * h) by DIFF_1:def_6
.= (((fdif (f,h)) . 2) . x) / (h * (2 * h)) by XCMPLX_1:78
.= (((fdif (f,h)) . 2) . x) / (2 * (h ^2)) ;
hence  [!f,x,(x + h),(x + (2 * h))!] = (((fdif (f,h)) . 2) . x) / (2 * (h ^2)) ; ::_thesis: verum
end;

theorem Th3: :: DIFF_2:3
for x, h being Real
for f being Function of REAL,REAL holds [!f,(x - h),x!] = (((bdif (f,h)) . 1) . x) / h
proof
let x, h be Real; ::_thesis: for f being Function of REAL,REAL holds [!f,(x - h),x!] = (((bdif (f,h)) . 1) . x) / h
let f be Function of REAL,REAL; ::_thesis: [!f,(x - h),x!] = (((bdif (f,h)) . 1) . x) / h
[!f,(x - h),x!] = [!f,x,(x - h)!] by DIFF_1:29
.= ((bD (f,h)) . x) / h by DIFF_1:4
.= ((bD (((bdif (f,h)) . 0),h)) . x) / h by DIFF_1:def_7
.= (((bdif (f,h)) . (0 + 1)) . x) / h by DIFF_1:def_7 ;
hence  [!f,(x - h),x!] = (((bdif (f,h)) . 1) . x) / h ; ::_thesis: verum
end;

theorem :: DIFF_2:4
for h, x being Real
for f being Function of REAL,REAL st h <> 0 holds
[!f,(x - (2 * h)),(x - h),x!] = (((bdif (f,h)) . 2) . x) / (2 * (h ^2))
proof
let h, x be Real; ::_thesis: for f being Function of REAL,REAL st h <> 0 holds
[!f,(x - (2 * h)),(x - h),x!] = (((bdif (f,h)) . 2) . x) / (2 * (h ^2))
let f be Function of REAL,REAL; ::_thesis: ( h <> 0 implies [!f,(x - (2 * h)),(x - h),x!] = (((bdif (f,h)) . 2) . x) / (2 * (h ^2)) )
set y = x - h;
A1: (bdif (f,h)) . 1 is Function of REAL,REAL by DIFF_1:12;
assume A2: h <> 0 ; ::_thesis: [!f,(x - (2 * h)),(x - h),x!] = (((bdif (f,h)) . 2) . x) / (2 * (h ^2))
then A3: x - h <> x - (2 * h) ;
 ( x <> x - h & x <> x - (2 * h) ) by A2;
then  x,x - h,x - (2 * h) are_mutually_different by A3, ZFMISC_1:def_5;
then [!f,(x - (2 * h)),(x - h),x!] = [!f,x,(x - h),(x - (2 * h))!] by DIFF_1:34
.= ([!f,(x - h),x!] - [!f,(x - h),(x - (2 * h))!]) / (x - (x - (2 * h))) by DIFF_1:29
.= (((((bdif (f,h)) . 1) . x) / h) - [!f,(x - h),(x - (2 * h))!]) / (x - (x - (2 * h))) by Th3
.= (((((bdif (f,h)) . 1) . x) / h) - [!f,((x - h) - h),(x - h)!]) / (x - (x - (2 * h))) by DIFF_1:29
.= (((((bdif (f,h)) . 1) . x) / h) - ((((bdif (f,h)) . 1) . (x - h)) / h)) / (x - (x - (2 * h))) by Th3
.= (((((bdif (f,h)) . 1) . x) - (((bdif (f,h)) . 1) . (x - h))) / h) / (x - (x - (2 * h))) by XCMPLX_1:120
.= (((bD (((bdif (f,h)) . 1),h)) . x) / h) / (2 * h) by A1, DIFF_1:4
.= ((((bdif (f,h)) . (1 + 1)) . x) / h) / (2 * h) by DIFF_1:def_7
.= (((bdif (f,h)) . 2) . x) / (h * (2 * h)) by XCMPLX_1:78
.= (((bdif (f,h)) . 2) . x) / (2 * (h ^2)) ;
hence  [!f,(x - (2 * h)),(x - h),x!] = (((bdif (f,h)) . 2) . x) / (2 * (h ^2)) ; ::_thesis: verum
end;

theorem Th5: :: DIFF_2:5
for r, x0, x1, x2 being Real
for f being Function of REAL,REAL holds [!(r (#) f),x0,x1,x2!] = r * [!f,x0,x1,x2!]
proof
let r, x0, x1, x2 be Real; ::_thesis: for f being Function of REAL,REAL holds [!(r (#) f),x0,x1,x2!] = r * [!f,x0,x1,x2!]
let f be Function of REAL,REAL; ::_thesis: [!(r (#) f),x0,x1,x2!] = r * [!f,x0,x1,x2!]
[!(r (#) f),x0,x1,x2!] = ((r * [!f,x0,x1!]) - [!(r (#) f),x1,x2!]) / (x0 - x2) by DIFF_1:31
.= ((r * [!f,x0,x1!]) - (r * [!f,x1,x2!])) / (x0 - x2) by DIFF_1:31
.= (r * ([!f,x0,x1!] - [!f,x1,x2!])) / (x0 - x2) ;
hence  [!(r (#) f),x0,x1,x2!] = r * [!f,x0,x1,x2!] by XCMPLX_1:74; ::_thesis: verum
end;

theorem Th6: :: DIFF_2:6
for x0, x1, x2 being Real
for f1, f2 being Function of REAL,REAL holds [!(f1 + f2),x0,x1,x2!] = [!f1,x0,x1,x2!] + [!f2,x0,x1,x2!]
proof
let x0, x1, x2 be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds [!(f1 + f2),x0,x1,x2!] = [!f1,x0,x1,x2!] + [!f2,x0,x1,x2!]
let f1, f2 be Function of REAL,REAL; ::_thesis: [!(f1 + f2),x0,x1,x2!] = [!f1,x0,x1,x2!] + [!f2,x0,x1,x2!]
[!(f1 + f2),x0,x1,x2!] = (([!f1,x0,x1!] + [!f2,x0,x1!]) - [!(f1 + f2),x1,x2!]) / (x0 - x2) by DIFF_1:32
.= (([!f1,x0,x1!] + [!f2,x0,x1!]) - ([!f1,x1,x2!] + [!f2,x1,x2!])) / (x0 - x2) by DIFF_1:32
.= (([!f1,x0,x1!] - [!f1,x1,x2!]) + ([!f2,x0,x1!] - [!f2,x1,x2!])) / (x0 - x2) ;
hence  [!(f1 + f2),x0,x1,x2!] = [!f1,x0,x1,x2!] + [!f2,x0,x1,x2!] by XCMPLX_1:62; ::_thesis: verum
end;

theorem :: DIFF_2:7
for r1, r2, x0, x1, x2 being Real
for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2!] = (r1 * [!f1,x0,x1,x2!]) + (r2 * [!f2,x0,x1,x2!])
proof
let r1, r2, x0, x1, x2 be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2!] = (r1 * [!f1,x0,x1,x2!]) + (r2 * [!f2,x0,x1,x2!])
let f1, f2 be Function of REAL,REAL; ::_thesis: [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2!] = (r1 * [!f1,x0,x1,x2!]) + (r2 * [!f2,x0,x1,x2!])
[!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2!] = [!(r1 (#) f1),x0,x1,x2!] + [!(r2 (#) f2),x0,x1,x2!] by Th6
.= (r1 * [!f1,x0,x1,x2!]) + [!(r2 (#) f2),x0,x1,x2!] by Th5 ;
hence  [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2!] = (r1 * [!f1,x0,x1,x2!]) + (r2 * [!f2,x0,x1,x2!]) by Th5; ::_thesis: verum
end;

theorem Th8: :: DIFF_2:8
for r, x0, x1, x2, x3 being Real
for f being Function of REAL,REAL holds [!(r (#) f),x0,x1,x2,x3!] = r * [!f,x0,x1,x2,x3!]
proof
let r, x0, x1, x2, x3 be Real; ::_thesis: for f being Function of REAL,REAL holds [!(r (#) f),x0,x1,x2,x3!] = r * [!f,x0,x1,x2,x3!]
let f be Function of REAL,REAL; ::_thesis: [!(r (#) f),x0,x1,x2,x3!] = r * [!f,x0,x1,x2,x3!]
[!(r (#) f),x0,x1,x2,x3!] = ((r * [!f,x0,x1,x2!]) - [!(r (#) f),x1,x2,x3!]) / (x0 - x3) by Th5
.= ((r * [!f,x0,x1,x2!]) - (r * [!f,x1,x2,x3!])) / (x0 - x3) by Th5
.= (r * ([!f,x0,x1,x2!] - [!f,x1,x2,x3!])) / (x0 - x3) ;
hence  [!(r (#) f),x0,x1,x2,x3!] = r * [!f,x0,x1,x2,x3!] by XCMPLX_1:74; ::_thesis: verum
end;

theorem Th9: :: DIFF_2:9
for x0, x1, x2, x3 being Real
for f1, f2 being Function of REAL,REAL holds [!(f1 + f2),x0,x1,x2,x3!] = [!f1,x0,x1,x2,x3!] + [!f2,x0,x1,x2,x3!]
proof
let x0, x1, x2, x3 be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds [!(f1 + f2),x0,x1,x2,x3!] = [!f1,x0,x1,x2,x3!] + [!f2,x0,x1,x2,x3!]
let f1, f2 be Function of REAL,REAL; ::_thesis: [!(f1 + f2),x0,x1,x2,x3!] = [!f1,x0,x1,x2,x3!] + [!f2,x0,x1,x2,x3!]
[!(f1 + f2),x0,x1,x2,x3!] = (([!f1,x0,x1,x2!] + [!f2,x0,x1,x2!]) - [!(f1 + f2),x1,x2,x3!]) / (x0 - x3) by Th6
.= (([!f1,x0,x1,x2!] + [!f2,x0,x1,x2!]) - ([!f1,x1,x2,x3!] + [!f2,x1,x2,x3!])) / (x0 - x3) by Th6
.= (([!f1,x0,x1,x2!] - [!f1,x1,x2,x3!]) + ([!f2,x0,x1,x2!] - [!f2,x1,x2,x3!])) / (x0 - x3) ;
hence  [!(f1 + f2),x0,x1,x2,x3!] = [!f1,x0,x1,x2,x3!] + [!f2,x0,x1,x2,x3!] by XCMPLX_1:62; ::_thesis: verum
end;

theorem :: DIFF_2:10
for r1, r2, x0, x1, x2, x3 being Real
for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3!] = (r1 * [!f1,x0,x1,x2,x3!]) + (r2 * [!f2,x0,x1,x2,x3!])
proof
let r1, r2, x0, x1, x2, x3 be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3!] = (r1 * [!f1,x0,x1,x2,x3!]) + (r2 * [!f2,x0,x1,x2,x3!])
let f1, f2 be Function of REAL,REAL; ::_thesis: [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3!] = (r1 * [!f1,x0,x1,x2,x3!]) + (r2 * [!f2,x0,x1,x2,x3!])
[!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3!] = [!(r1 (#) f1),x0,x1,x2,x3!] + [!(r2 (#) f2),x0,x1,x2,x3!] by Th9
.= (r1 * [!f1,x0,x1,x2,x3!]) + [!(r2 (#) f2),x0,x1,x2,x3!] by Th8 ;
hence  [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3!] = (r1 * [!f1,x0,x1,x2,x3!]) + (r2 * [!f2,x0,x1,x2,x3!]) by Th8; ::_thesis: verum
end;

definition
let f be real-valued Function;
let x0, x1, x2, x3, x4 be real number ;
func[!f,x0,x1,x2,x3,x4!] ->  Real equals :: DIFF_2:def 1
([!f,x0,x1,x2,x3!] - [!f,x1,x2,x3,x4!]) / (x0 - x4);
correctness
coherence
([!f,x0,x1,x2,x3!] - [!f,x1,x2,x3,x4!]) / (x0 - x4) is Real;
;
end;

:: deftheorem  defines [! DIFF_2:def_1_:_
 for f being real-valued Function
for x0, x1, x2, x3, x4 being real number holds [!f,x0,x1,x2,x3,x4!] = ([!f,x0,x1,x2,x3!] - [!f,x1,x2,x3,x4!]) / (x0 - x4);

theorem Th11: :: DIFF_2:11
for r, x0, x1, x2, x3, x4 being Real
for f being Function of REAL,REAL holds [!(r (#) f),x0,x1,x2,x3,x4!] = r * [!f,x0,x1,x2,x3,x4!]
proof
let r, x0, x1, x2, x3, x4 be Real; ::_thesis: for f being Function of REAL,REAL holds [!(r (#) f),x0,x1,x2,x3,x4!] = r * [!f,x0,x1,x2,x3,x4!]
let f be Function of REAL,REAL; ::_thesis: [!(r (#) f),x0,x1,x2,x3,x4!] = r * [!f,x0,x1,x2,x3,x4!]
[!(r (#) f),x0,x1,x2,x3,x4!] = ((r * [!f,x0,x1,x2,x3!]) - [!(r (#) f),x1,x2,x3,x4!]) / (x0 - x4) by Th8
.= ((r * [!f,x0,x1,x2,x3!]) - (r * [!f,x1,x2,x3,x4!])) / (x0 - x4) by Th8
.= (r * ([!f,x0,x1,x2,x3!] - [!f,x1,x2,x3,x4!])) / (x0 - x4) ;
hence  [!(r (#) f),x0,x1,x2,x3,x4!] = r * [!f,x0,x1,x2,x3,x4!] by XCMPLX_1:74; ::_thesis: verum
end;

theorem Th12: :: DIFF_2:12
for x0, x1, x2, x3, x4 being Real
for f1, f2 being Function of REAL,REAL holds [!(f1 + f2),x0,x1,x2,x3,x4!] = [!f1,x0,x1,x2,x3,x4!] + [!f2,x0,x1,x2,x3,x4!]
proof
let x0, x1, x2, x3, x4 be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds [!(f1 + f2),x0,x1,x2,x3,x4!] = [!f1,x0,x1,x2,x3,x4!] + [!f2,x0,x1,x2,x3,x4!]
let f1, f2 be Function of REAL,REAL; ::_thesis: [!(f1 + f2),x0,x1,x2,x3,x4!] = [!f1,x0,x1,x2,x3,x4!] + [!f2,x0,x1,x2,x3,x4!]
[!(f1 + f2),x0,x1,x2,x3,x4!] = (([!f1,x0,x1,x2,x3!] + [!f2,x0,x1,x2,x3!]) - [!(f1 + f2),x1,x2,x3,x4!]) / (x0 - x4) by Th9
.= (([!f1,x0,x1,x2,x3!] + [!f2,x0,x1,x2,x3!]) - ([!f1,x1,x2,x3,x4!] + [!f2,x1,x2,x3,x4!])) / (x0 - x4) by Th9
.= (([!f1,x0,x1,x2,x3!] - [!f1,x1,x2,x3,x4!]) + ([!f2,x0,x1,x2,x3!] - [!f2,x1,x2,x3,x4!])) / (x0 - x4) ;
hence  [!(f1 + f2),x0,x1,x2,x3,x4!] = [!f1,x0,x1,x2,x3,x4!] + [!f2,x0,x1,x2,x3,x4!] by XCMPLX_1:62; ::_thesis: verum
end;

theorem :: DIFF_2:13
for r1, r2, x0, x1, x2, x3, x4 being Real
for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4!] = (r1 * [!f1,x0,x1,x2,x3,x4!]) + (r2 * [!f2,x0,x1,x2,x3,x4!])
proof
let r1, r2, x0, x1, x2, x3, x4 be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4!] = (r1 * [!f1,x0,x1,x2,x3,x4!]) + (r2 * [!f2,x0,x1,x2,x3,x4!])
let f1, f2 be Function of REAL,REAL; ::_thesis: [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4!] = (r1 * [!f1,x0,x1,x2,x3,x4!]) + (r2 * [!f2,x0,x1,x2,x3,x4!])
[!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4!] = [!(r1 (#) f1),x0,x1,x2,x3,x4!] + [!(r2 (#) f2),x0,x1,x2,x3,x4!] by Th12
.= (r1 * [!f1,x0,x1,x2,x3,x4!]) + [!(r2 (#) f2),x0,x1,x2,x3,x4!] by Th11 ;
hence  [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4!] = (r1 * [!f1,x0,x1,x2,x3,x4!]) + (r2 * [!f2,x0,x1,x2,x3,x4!]) by Th11; ::_thesis: verum
end;

definition
let f be real-valued Function;
let x0, x1, x2, x3, x4, x5 be real number ;
func[!f,x0,x1,x2,x3,x4,x5!] ->  Real equals :: DIFF_2:def 2
([!f,x0,x1,x2,x3,x4!] - [!f,x1,x2,x3,x4,x5!]) / (x0 - x5);
correctness
coherence
([!f,x0,x1,x2,x3,x4!] - [!f,x1,x2,x3,x4,x5!]) / (x0 - x5) is Real;
;
end;

:: deftheorem  defines [! DIFF_2:def_2_:_
 for f being real-valued Function
for x0, x1, x2, x3, x4, x5 being real number holds [!f,x0,x1,x2,x3,x4,x5!] = ([!f,x0,x1,x2,x3,x4!] - [!f,x1,x2,x3,x4,x5!]) / (x0 - x5);

theorem Th14: :: DIFF_2:14
for r, x0, x1, x2, x3, x4, x5 being Real
for f being Function of REAL,REAL holds [!(r (#) f),x0,x1,x2,x3,x4,x5!] = r * [!f,x0,x1,x2,x3,x4,x5!]
proof
let r, x0, x1, x2, x3, x4, x5 be Real; ::_thesis: for f being Function of REAL,REAL holds [!(r (#) f),x0,x1,x2,x3,x4,x5!] = r * [!f,x0,x1,x2,x3,x4,x5!]
let f be Function of REAL,REAL; ::_thesis: [!(r (#) f),x0,x1,x2,x3,x4,x5!] = r * [!f,x0,x1,x2,x3,x4,x5!]
[!(r (#) f),x0,x1,x2,x3,x4,x5!] = ((r * [!f,x0,x1,x2,x3,x4!]) - [!(r (#) f),x1,x2,x3,x4,x5!]) / (x0 - x5) by Th11
.= ((r * [!f,x0,x1,x2,x3,x4!]) - (r * [!f,x1,x2,x3,x4,x5!])) / (x0 - x5) by Th11
.= (r * ([!f,x0,x1,x2,x3,x4!] - [!f,x1,x2,x3,x4,x5!])) / (x0 - x5) ;
hence  [!(r (#) f),x0,x1,x2,x3,x4,x5!] = r * [!f,x0,x1,x2,x3,x4,x5!] by XCMPLX_1:74; ::_thesis: verum
end;

theorem Th15: :: DIFF_2:15
for x0, x1, x2, x3, x4, x5 being Real
for f1, f2 being Function of REAL,REAL holds [!(f1 + f2),x0,x1,x2,x3,x4,x5!] = [!f1,x0,x1,x2,x3,x4,x5!] + [!f2,x0,x1,x2,x3,x4,x5!]
proof
let x0, x1, x2, x3, x4, x5 be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds [!(f1 + f2),x0,x1,x2,x3,x4,x5!] = [!f1,x0,x1,x2,x3,x4,x5!] + [!f2,x0,x1,x2,x3,x4,x5!]
let f1, f2 be Function of REAL,REAL; ::_thesis: [!(f1 + f2),x0,x1,x2,x3,x4,x5!] = [!f1,x0,x1,x2,x3,x4,x5!] + [!f2,x0,x1,x2,x3,x4,x5!]
[!(f1 + f2),x0,x1,x2,x3,x4,x5!] = (([!f1,x0,x1,x2,x3,x4!] + [!f2,x0,x1,x2,x3,x4!]) - [!(f1 + f2),x1,x2,x3,x4,x5!]) / (x0 - x5) by Th12
.= (([!f1,x0,x1,x2,x3,x4!] + [!f2,x0,x1,x2,x3,x4!]) - ([!f1,x1,x2,x3,x4,x5!] + [!f2,x1,x2,x3,x4,x5!])) / (x0 - x5) by Th12
.= (([!f1,x0,x1,x2,x3,x4!] - [!f1,x1,x2,x3,x4,x5!]) + ([!f2,x0,x1,x2,x3,x4!] - [!f2,x1,x2,x3,x4,x5!])) / (x0 - x5) ;
hence  [!(f1 + f2),x0,x1,x2,x3,x4,x5!] = [!f1,x0,x1,x2,x3,x4,x5!] + [!f2,x0,x1,x2,x3,x4,x5!] by XCMPLX_1:62; ::_thesis: verum
end;

theorem :: DIFF_2:16
for r1, r2, x0, x1, x2, x3, x4, x5 being Real
for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4,x5!] = (r1 * [!f1,x0,x1,x2,x3,x4,x5!]) + (r2 * [!f2,x0,x1,x2,x3,x4,x5!])
proof
let r1, r2, x0, x1, x2, x3, x4, x5 be Real; ::_thesis: for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4,x5!] = (r1 * [!f1,x0,x1,x2,x3,x4,x5!]) + (r2 * [!f2,x0,x1,x2,x3,x4,x5!])
let f1, f2 be Function of REAL,REAL; ::_thesis: [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4,x5!] = (r1 * [!f1,x0,x1,x2,x3,x4,x5!]) + (r2 * [!f2,x0,x1,x2,x3,x4,x5!])
[!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4,x5!] = [!(r1 (#) f1),x0,x1,x2,x3,x4,x5!] + [!(r2 (#) f2),x0,x1,x2,x3,x4,x5!] by Th15
.= (r1 * [!f1,x0,x1,x2,x3,x4,x5!]) + [!(r2 (#) f2),x0,x1,x2,x3,x4,x5!] by Th14 ;
hence  [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4,x5!] = (r1 * [!f1,x0,x1,x2,x3,x4,x5!]) + (r2 * [!f2,x0,x1,x2,x3,x4,x5!]) by Th14; ::_thesis: verum
end;

theorem :: DIFF_2:17
for x0, x1, x2 being Real
for f being Function of REAL,REAL st x0,x1,x2 are_mutually_different holds
[!f,x0,x1,x2!] = (((f . x0) / ((x0 - x1) * (x0 - x2))) + ((f . x1) / ((x1 - x0) * (x1 - x2)))) + ((f . x2) / ((x2 - x0) * (x2 - x1)))
proof
let x0, x1, x2 be Real; ::_thesis: for f being Function of REAL,REAL st x0,x1,x2 are_mutually_different holds
[!f,x0,x1,x2!] = (((f . x0) / ((x0 - x1) * (x0 - x2))) + ((f . x1) / ((x1 - x0) * (x1 - x2)))) + ((f . x2) / ((x2 - x0) * (x2 - x1)))
let f be Function of REAL,REAL; ::_thesis: ( x0,x1,x2 are_mutually_different implies [!f,x0,x1,x2!] = (((f . x0) / ((x0 - x1) * (x0 - x2))) + ((f . x1) / ((x1 - x0) * (x1 - x2)))) + ((f . x2) / ((x2 - x0) * (x2 - x1))) )
assume A1: x0,x1,x2 are_mutually_different ; ::_thesis: [!f,x0,x1,x2!] = (((f . x0) / ((x0 - x1) * (x0 - x2))) + ((f . x1) / ((x1 - x0) * (x1 - x2)))) + ((f . x2) / ((x2 - x0) * (x2 - x1)))
then A2: x1 - x2 <> 0 by ZFMISC_1:def_5;
A3: x0 - x1 <> 0 by A1, ZFMISC_1:def_5;
A4: x0 - x2 <> 0 by A1, ZFMISC_1:def_5;
[!f,x0,x1,x2!] = ((((f . x0) - (f . x1)) / (x0 - x1)) / (x0 - x2)) - ((((f . x1) - (f . x2)) / (x1 - x2)) / (x0 - x2)) by XCMPLX_1:120
.= (((f . x0) - (f . x1)) / ((x0 - x1) * (x0 - x2))) - ((((f . x1) - (f . x2)) / (x1 - x2)) / (x0 - x2)) by XCMPLX_1:78
.= (((f . x0) - (f . x1)) / ((x0 - x1) * (x0 - x2))) - (((f . x1) - (f . x2)) / ((x1 - x2) * (x0 - x2))) by XCMPLX_1:78
.= (((f . x0) / ((x0 - x1) * (x0 - x2))) - ((f . x1) / ((x0 - x1) * (x0 - x2)))) - (((f . x1) - (f . x2)) / ((x1 - x2) * (x0 - x2))) by XCMPLX_1:120
.= (((f . x0) / ((x0 - x1) * (x0 - x2))) - ((f . x1) / ((x0 - x1) * (x0 - x2)))) - (((f . x1) / ((x1 - x2) * (x0 - x2))) - ((f . x2) / ((x1 - x2) * (x0 - x2)))) by XCMPLX_1:120
.= (((f . x0) / ((x0 - x1) * (x0 - x2))) - (((f . x1) / ((x0 - x1) * (x0 - x2))) + ((f . x1) / ((x1 - x2) * (x0 - x2))))) + ((f . x2) / ((x1 - x2) * (x0 - x2)))
.= (((f . x0) / ((x0 - x1) * (x0 - x2))) - ((((f . x1) * (x1 - x2)) / (((x0 - x1) * (x0 - x2)) * (x1 - x2))) + ((f . x1) / ((x1 - x2) * (x0 - x2))))) + ((f . x2) / ((x1 - x2) * (x0 - x2))) by A2, XCMPLX_1:91
.= (((f . x0) / ((x0 - x1) * (x0 - x2))) - ((((f . x1) * (x1 - x2)) / (((x0 - x1) * (x0 - x2)) * (x1 - x2))) + (((f . x1) * (x0 - x1)) / (((x1 - x2) * (x0 - x2)) * (x0 - x1))))) + ((f . x2) / ((x1 - x2) * (x0 - x2))) by A3, XCMPLX_1:91
.= (((f . x0) / ((x0 - x1) * (x0 - x2))) - ((((f . x1) * (x1 - x2)) + ((f . x1) * (x0 - x1))) / (((x0 - x1) * (x0 - x2)) * (x1 - x2)))) + ((f . x2) / ((x1 - x2) * (x0 - x2))) by XCMPLX_1:62
.= (((f . x0) / ((x0 - x1) * (x0 - x2))) - (((f . x1) * (x0 - x2)) / (((x0 - x1) * (x1 - x2)) * (x0 - x2)))) + ((f . x2) / ((x1 - x2) * (x0 - x2)))
.= (((f . x0) / ((x0 - x1) * (x0 - x2))) - ((f . x1) / (- ((x1 - x0) * (x1 - x2))))) + ((f . x2) / (- ((x2 - x1) * (x0 - x2)))) by A4, XCMPLX_1:91
.= (((f . x0) / ((x0 - x1) * (x0 - x2))) + (- ((f . x1) / (- ((x1 - x0) * (x1 - x2)))))) + ((f . x2) / ((- (x2 - x1)) * (- (x2 - x0)))) ;
hence  [!f,x0,x1,x2!] = (((f . x0) / ((x0 - x1) * (x0 - x2))) + ((f . x1) / ((x1 - x0) * (x1 - x2)))) + ((f . x2) / ((x2 - x0) * (x2 - x1))) by XCMPLX_1:189; ::_thesis: verum
end;

theorem :: DIFF_2:18
for x0, x1, x2, x3 being Real
for f being Function of REAL,REAL st x0,x1,x2,x3 are_mutually_different holds
( [!f,x0,x1,x2,x3!] = [!f,x1,x2,x3,x0!] & [!f,x0,x1,x2,x3!] = [!f,x3,x2,x1,x0!] )
proof
let x0, x1, x2, x3 be Real; ::_thesis: for f being Function of REAL,REAL st x0,x1,x2,x3 are_mutually_different holds
( [!f,x0,x1,x2,x3!] = [!f,x1,x2,x3,x0!] & [!f,x0,x1,x2,x3!] = [!f,x3,x2,x1,x0!] )
let f be Function of REAL,REAL; ::_thesis: ( x0,x1,x2,x3 are_mutually_different implies ( [!f,x0,x1,x2,x3!] = [!f,x1,x2,x3,x0!] & [!f,x0,x1,x2,x3!] = [!f,x3,x2,x1,x0!] ) )
set x10 = x1 - x0;
set x20 = x2 - x0;
set x30 = x3 - x0;
set x12 = x1 - x2;
set x13 = x1 - x3;
set x23 = x2 - x3;
assume A1: x0,x1,x2,x3 are_mutually_different ; ::_thesis: ( [!f,x0,x1,x2,x3!] = [!f,x1,x2,x3,x0!] & [!f,x0,x1,x2,x3!] = [!f,x3,x2,x1,x0!] )
then A2: x2 - x3 <> 0 by ZFMISC_1:def_6;
A3: x3 - x0 <> 0 by A1, ZFMISC_1:def_6;
A4: x1 - x3 <> 0 by A1, ZFMISC_1:def_6;
A5: x1 - x0 <> 0 by A1, ZFMISC_1:def_6;
A6: x2 - x0 <> 0 by A1, ZFMISC_1:def_6;
A7: x1 - x2 <> 0 by A1, ZFMISC_1:def_6;
A8: [!f,x0,x1,x2,x3!] = ((((((f . x0) - (f . x1)) / (- (x1 - x0))) - (((f . x1) - (f . x2)) / (x1 - x2))) / (- (x2 - x0))) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3)
.= ((((- (((f . x0) - (f . x1)) / (x1 - x0))) - (((f . x1) - (f . x2)) / (x1 - x2))) / (- (x2 - x0))) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3) by XCMPLX_1:188
.= (((- ((((f . x0) - (f . x1)) / (x1 - x0)) + (((f . x1) - (f . x2)) / (x1 - x2)))) / (- (x2 - x0))) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3)
.= ((((((f . x0) - (f . x1)) / (x1 - x0)) + (((f . x1) - (f . x2)) / (x1 - x2))) / (x2 - x0)) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3) by XCMPLX_1:191
.= (((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((x1 - x0) * (x1 - x2))) / (x2 - x0)) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3) by A7, A5, XCMPLX_1:116
.= (((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((x1 - x0) * (x1 - x2))) / (x2 - x0)) - ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((x1 - x2) * (x2 - x3))) / (x1 - x3))) / (x0 - x3) by A2, A7, XCMPLX_1:130
.= ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) - ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((x1 - x2) * (x2 - x3))) / (x1 - x3))) / (x0 - x3) by XCMPLX_1:78
.= ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) - (((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3)))) / (x0 - x3) by XCMPLX_1:78
.= (- ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) - (((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))))) / (- (x0 - x3)) by XCMPLX_1:191
.= ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))) - (((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0)))) / (x3 - x0)
.= ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))) / (x3 - x0)) - ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) / (x3 - x0)) by XCMPLX_1:120
.= (((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x3 - x0))) - ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) / (x3 - x0)) by XCMPLX_1:78
.= (((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x3 - x0))) - (((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((((x1 - x0) * (x1 - x2)) * (x2 - x0)) * (x3 - x0))) by XCMPLX_1:78
.= ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) * (x2 - x0)) / (((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x3 - x0)) * (x2 - x0))) - (((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((((x1 - x0) * (x1 - x2)) * (x2 - x0)) * (x3 - x0))) by A6, XCMPLX_1:91
.= (((((((f . x1) - (f . x2)) * (x2 - x3)) * (x2 - x0)) - ((((f . x2) - (f . x3)) * (x1 - x2)) * (x2 - x0))) * (x1 - x0)) / ((((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x0))) - (((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((((x1 - x0) * (x1 - x2)) * (x2 - x0)) * (x3 - x0))) by A5, XCMPLX_1:91
.= (((((((f . x1) - (f . x2)) * (x2 - x3)) * (x2 - x0)) * (x1 - x0)) - (((((f . x2) - (f . x3)) * (x1 - x2)) * (x2 - x0)) * (x1 - x0))) / ((((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x0))) - ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) * ((x2 - x3) * (x1 - x3))) / (((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x1 - x0)) * ((x2 - x3) * (x1 - x3)))) by A2, A4, XCMPLX_1:6, XCMPLX_1:91
.= (((((((f . x1) - (f . x2)) * (x2 - x3)) * (x2 - x0)) * (x1 - x0)) - (((((f . x2) - (f . x3)) * (x1 - x2)) * (x2 - x0)) * (x1 - x0))) - ((((((f . x0) - (f . x1)) * (x1 - x2)) * (x2 - x3)) * (x1 - x3)) + (((((f . x1) - (f . x2)) * (x1 - x0)) * (x2 - x3)) * (x1 - x3)))) / ((((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x0)) by XCMPLX_1:120
.= ((((- ((((f . x0) * (x1 - x2)) * (x2 - x3)) * (x1 - x3))) + ((((f . x1) * (x2 - x0)) * (x2 - x3)) * (x3 - x0))) - ((((f . x2) * (x1 - x3)) * (x1 - x0)) * (x3 - x0))) + ((((f . x3) * (x1 - x2)) * (x2 - x0)) * (x1 - x0))) / ((((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x0)) ;
A9: [!f,x3,x2,x1,x0!] = ((((((f . x3) - (f . x2)) / (- (x2 - x3))) - (((f . x2) - (f . x1)) / (- (x1 - x2)))) / (- (x1 - x3))) - (((((f . x2) - (f . x1)) / (- (x1 - x2))) - (((f . x1) - (f . x0)) / (x1 - x0))) / (x2 - x0))) / (x3 - x0)
.= ((((- (((f . x3) - (f . x2)) / (x2 - x3))) - (((f . x2) - (f . x1)) / (- (x1 - x2)))) / (- (x1 - x3))) - (((((f . x2) - (f . x1)) / (- (x1 - x2))) - (((f . x1) - (f . x0)) / (x1 - x0))) / (x2 - x0))) / (x3 - x0) by XCMPLX_1:188
.= ((((- (((f . x3) - (f . x2)) / (x2 - x3))) - (- (((f . x2) - (f . x1)) / (x1 - x2)))) / (- (x1 - x3))) - (((((f . x2) - (f . x1)) / (- (x1 - x2))) - (((f . x1) - (f . x0)) / (x1 - x0))) / (x2 - x0))) / (x3 - x0) by XCMPLX_1:188
.= (((- ((((f . x3) - (f . x2)) / (x2 - x3)) - (((f . x2) - (f . x1)) / (x1 - x2)))) / (- (x1 - x3))) - (((((f . x2) - (f . x1)) / (- (x1 - x2))) - (((f . x1) - (f . x0)) / (x1 - x0))) / (x2 - x0))) / (x3 - x0)
.= ((((((f . x3) - (f . x2)) / (x2 - x3)) - (((f . x2) - (f . x1)) / (x1 - x2))) / (x1 - x3)) - (((((f . x2) - (f . x1)) / (- (x1 - x2))) - (((f . x1) - (f . x0)) / (x1 - x0))) / (x2 - x0))) / (x3 - x0) by XCMPLX_1:191
.= ((((((f . x3) - (f . x2)) / (x2 - x3)) - (((f . x2) - (f . x1)) / (x1 - x2))) / (x1 - x3)) - (((- (((f . x2) - (f . x1)) / (x1 - x2))) - (((f . x1) - (f . x0)) / (x1 - x0))) / (x2 - x0))) / (x3 - x0) by XCMPLX_1:188
.= ((((((f . x3) - (f . x2)) / (x2 - x3)) - (((f . x2) - (f . x1)) / (x1 - x2))) / (x1 - x3)) + (- ((- ((((f . x1) - (f . x0)) / (x1 - x0)) + (((f . x2) - (f . x1)) / (x1 - x2)))) / (x2 - x0)))) / (x3 - x0)
.= ((((((f . x3) - (f . x2)) / (x2 - x3)) - (((f . x2) - (f . x1)) / (x1 - x2))) / (x1 - x3)) + (((((f . x1) - (f . x0)) / (x1 - x0)) + (((f . x2) - (f . x1)) / (x1 - x2))) / (x2 - x0))) / (x3 - x0) by XCMPLX_1:190
.= (((((((f . x3) - (f . x2)) * (x1 - x2)) - (((f . x2) - (f . x1)) * (x2 - x3))) / ((x2 - x3) * (x1 - x2))) / (x1 - x3)) + (((((f . x1) - (f . x0)) / (x1 - x0)) + (((f . x2) - (f . x1)) / (x1 - x2))) / (x2 - x0))) / (x3 - x0) by A2, A7, XCMPLX_1:130
.= (((((((f . x3) - (f . x2)) * (x1 - x2)) - (((f . x2) - (f . x1)) * (x2 - x3))) / ((x2 - x3) * (x1 - x2))) / (x1 - x3)) + ((((((f . x1) - (f . x0)) * (x1 - x2)) + (((f . x2) - (f . x1)) * (x1 - x0))) / ((x1 - x0) * (x1 - x2))) / (x2 - x0))) / (x3 - x0) by A7, A5, XCMPLX_1:116
.= ((((((f . x3) - (f . x2)) * (x1 - x2)) - (((f . x2) - (f . x1)) * (x2 - x3))) / (((x2 - x3) * (x1 - x2)) * (x1 - x3))) + ((((((f . x1) - (f . x0)) * (x1 - x2)) + (((f . x2) - (f . x1)) * (x1 - x0))) / ((x1 - x0) * (x1 - x2))) / (x2 - x0))) / (x3 - x0) by XCMPLX_1:78
.= ((((((f . x3) - (f . x2)) * (x1 - x2)) - (((f . x2) - (f . x1)) * (x2 - x3))) / (((x2 - x3) * (x1 - x2)) * (x1 - x3))) + (((((f . x1) - (f . x0)) * (x1 - x2)) + (((f . x2) - (f . x1)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0)))) / (x3 - x0) by XCMPLX_1:78
.= ((((((f . x3) - (f . x2)) * (x1 - x2)) - (((f . x2) - (f . x1)) * (x2 - x3))) / (((x2 - x3) * (x1 - x2)) * (x1 - x3))) + ((((((f . x1) - (f . x0)) * (x1 - x2)) + (((f . x2) - (f . x1)) * (x1 - x0))) * (x1 - x3)) / ((((x1 - x0) * (x1 - x2)) * (x2 - x0)) * (x1 - x3)))) / (x3 - x0) by A4, XCMPLX_1:91
.= ((((((f . x3) - (f . x2)) * (x1 - x2)) - (((f . x2) - (f . x1)) * (x2 - x3))) / (((x2 - x3) * (x1 - x2)) * (x1 - x3))) + (((((((f . x1) - (f . x0)) * (x1 - x2)) * (x1 - x3)) + ((((f . x2) - (f . x1)) * (x1 - x0)) * (x1 - x3))) * (x2 - x3)) / (((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)))) / (x3 - x0) by A2, XCMPLX_1:91
.= (((((((f . x3) - (f . x2)) * (x1 - x2)) - (((f . x2) - (f . x1)) * (x2 - x3))) * (x2 - x0)) / ((((x2 - x3) * (x1 - x2)) * (x1 - x3)) * (x2 - x0))) + (((((((f . x1) - (f . x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) + (((((f . x2) - (f . x1)) * (x1 - x0)) * (x1 - x3)) * (x2 - x3))) / (((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)))) / (x3 - x0) by A6, XCMPLX_1:91
.= ((((((((f . x3) - (f . x2)) * (x1 - x2)) * (x2 - x0)) - ((((f . x2) - (f . x1)) * (x2 - x3)) * (x2 - x0))) * (x1 - x0)) / (((((x1 - x2) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)) * (x1 - x0))) + (((((((f . x1) - (f . x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) + (((((f . x2) - (f . x1)) * (x1 - x0)) * (x1 - x3)) * (x2 - x3))) / (((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)))) / (x3 - x0) by A5, XCMPLX_1:91
.= ((((((((f . x3) - (f . x2)) * (x1 - x2)) * (x2 - x0)) * (x1 - x0)) - (((((f . x2) - (f . x1)) * (x2 - x3)) * (x2 - x0)) * (x1 - x0))) / (((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3))) / (x3 - x0)) + ((((((((f . x1) - (f . x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) + (((((f . x2) - (f . x1)) * (x1 - x0)) * (x1 - x3)) * (x2 - x3))) / (((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3))) / (x3 - x0)) by XCMPLX_1:62
.= (((((((f . x3) - (f . x2)) * (x1 - x2)) * (x2 - x0)) * (x1 - x0)) - (((((f . x2) - (f . x1)) * (x2 - x3)) * (x2 - x0)) * (x1 - x0))) / ((((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)) * (x3 - x0))) + ((((((((f . x1) - (f . x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) + (((((f . x2) - (f . x1)) * (x1 - x0)) * (x1 - x3)) * (x2 - x3))) / (((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3))) / (x3 - x0)) by XCMPLX_1:78
.= (((((((f . x3) - (f . x2)) * (x1 - x2)) * (x2 - x0)) * (x1 - x0)) - (((((f . x2) - (f . x1)) * (x2 - x3)) * (x2 - x0)) * (x1 - x0))) / ((((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)) * (x3 - x0))) + (((((((f . x1) - (f . x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) + (((((f . x2) - (f . x1)) * (x1 - x0)) * (x1 - x3)) * (x2 - x3))) / ((((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)) * (x3 - x0))) by XCMPLX_1:78
.= (((((((f . x3) - (f . x2)) * (x1 - x2)) * (x2 - x0)) * (x1 - x0)) - (((((f . x2) - (f . x1)) * (x2 - x3)) * (x2 - x0)) * (x1 - x0))) + ((((((f . x1) - (f . x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) + (((((f . x2) - (f . x1)) * (x1 - x0)) * (x1 - x3)) * (x2 - x3)))) / ((((((x1 - x0) * (x1 - x2)) * (x1 - x3)) * (x2 - x0)) * (x2 - x3)) * (x3 - x0)) by XCMPLX_1:62
.= [!f,x0,x1,x2,x3!] by A8 ;
[!f,x1,x2,x3,x0!] = (((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((x1 - x2) * (x2 - x3))) / (x1 - x3)) - (((((f . x2) - (f . x3)) / (x2 - x3)) - (((f . x3) - (f . x0)) / (x3 - x0))) / (x2 - x0))) / (x1 - x0) by A2, A7, XCMPLX_1:130
.= (((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((x1 - x2) * (x2 - x3))) / (x1 - x3)) - ((((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / ((x2 - x3) * (x3 - x0))) / (x2 - x0))) / (x1 - x0) by A2, A3, XCMPLX_1:130
.= ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))) - ((((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / ((x2 - x3) * (x3 - x0))) / (x2 - x0))) / (x1 - x0) by XCMPLX_1:78
.= ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))) - (((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / (((x2 - x3) * (x3 - x0)) * (x2 - x0)))) / (x1 - x0) by XCMPLX_1:78
.= ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))) / (x1 - x0)) - ((((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / (((x2 - x3) * (x3 - x0)) * (x2 - x0))) / (x1 - x0)) by XCMPLX_1:120
.= (((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x1 - x0))) - ((((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / (((x2 - x3) * (x3 - x0)) * (x2 - x0))) / (x1 - x0)) by XCMPLX_1:78
.= (((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x1 - x0))) - (((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / ((((x2 - x3) * (x3 - x0)) * (x2 - x0)) * (x1 - x0))) by XCMPLX_1:78
.= ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) * (x3 - x0)) / (((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x1 - x0)) * (x3 - x0))) - (((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / ((((x2 - x3) * (x3 - x0)) * (x2 - x0)) * (x1 - x0))) by A3, XCMPLX_1:91
.= (((((((f . x1) - (f . x2)) * (x2 - x3)) * (x3 - x0)) - ((((f . x2) - (f . x3)) * (x1 - x2)) * (x3 - x0))) * (x2 - x0)) / ((((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x1 - x0)) * (x3 - x0)) * (x2 - x0))) - (((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) / ((((x2 - x3) * (x3 - x0)) * (x2 - x0)) * (x1 - x0))) by A6, XCMPLX_1:91
.= (((((((f . x1) - (f . x2)) * (x2 - x3)) * (x3 - x0)) * (x2 - x0)) - (((((f . x2) - (f . x3)) * (x1 - x2)) * (x3 - x0)) * (x2 - x0))) / ((((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x1 - x0)) * (x3 - x0)) * (x2 - x0))) - ((((((f . x2) - (f . x3)) * (x3 - x0)) - (((f . x3) - (f . x0)) * (x2 - x3))) * (x1 - x3)) / (((((x1 - x0) * (x3 - x0)) * (x2 - x0)) * (x2 - x3)) * (x1 - x3))) by A4, XCMPLX_1:91
.= (((((((f . x1) - (f . x2)) * (x2 - x3)) * (x3 - x0)) * (x2 - x0)) - (((((f . x2) - (f . x3)) * (x1 - x2)) * (x3 - x0)) * (x2 - x0))) / ((((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x1 - x0)) * (x3 - x0)) * (x2 - x0))) - (((((((f . x2) - (f . x3)) * (x3 - x0)) * (x1 - x3)) - ((((f . x3) - (f . x0)) * (x2 - x3)) * (x1 - x3))) * (x1 - x2)) / ((((((x2 - x3) * (x1 - x3)) * (x1 - x0)) * (x3 - x0)) * (x2 - x0)) * (x1 - x2))) by A7, XCMPLX_1:91
.= (((((((f . x1) - (f . x2)) * (x2 - x3)) * (x3 - x0)) * (x2 - x0)) - (((((f . x2) - (f . x3)) * (x1 - x2)) * (x3 - x0)) * (x2 - x0))) - ((((((f . x2) - (f . x3)) * (x3 - x0)) * (x1 - x3)) * (x1 - x2)) - (((((f . x3) - (f . x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x2)))) / ((((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x1 - x0)) * (x3 - x0)) * (x2 - x0)) by XCMPLX_1:120
.= [!f,x0,x1,x2,x3!] by A8 ;
hence  ( [!f,x0,x1,x2,x3!] = [!f,x1,x2,x3,x0!] & [!f,x0,x1,x2,x3!] = [!f,x3,x2,x1,x0!] ) by A9; ::_thesis: verum
end;

theorem :: DIFF_2:19
for x0, x1, x2, x3 being Real
for f being Function of REAL,REAL st x0,x1,x2,x3 are_mutually_different holds
( [!f,x0,x1,x2,x3!] = [!f,x1,x0,x2,x3!] & [!f,x0,x1,x2,x3!] = [!f,x1,x2,x0,x3!] )
proof
let x0, x1, x2, x3 be Real; ::_thesis: for f being Function of REAL,REAL st x0,x1,x2,x3 are_mutually_different holds
( [!f,x0,x1,x2,x3!] = [!f,x1,x0,x2,x3!] & [!f,x0,x1,x2,x3!] = [!f,x1,x2,x0,x3!] )
let f be Function of REAL,REAL; ::_thesis: ( x0,x1,x2,x3 are_mutually_different implies ( [!f,x0,x1,x2,x3!] = [!f,x1,x0,x2,x3!] & [!f,x0,x1,x2,x3!] = [!f,x1,x2,x0,x3!] ) )
set x10 = x1 - x0;
set x20 = x2 - x0;
set x30 = x3 - x0;
set x12 = x1 - x2;
set x13 = x1 - x3;
set x23 = x2 - x3;
assume A1: x0,x1,x2,x3 are_mutually_different ; ::_thesis: ( [!f,x0,x1,x2,x3!] = [!f,x1,x0,x2,x3!] & [!f,x0,x1,x2,x3!] = [!f,x1,x2,x0,x3!] )
then A2: x2 - x3 <> 0 by ZFMISC_1:def_6;
A3: x1 - x3 <> 0 by A1, ZFMISC_1:def_6;
A4: x1 - x2 <> 0 by A1, ZFMISC_1:def_6;
A5: x3 - x0 <> 0 by A1, ZFMISC_1:def_6;
A6: x2 - x0 <> 0 by A1, ZFMISC_1:def_6;
A7: x1 - x0 <> 0 by A1, ZFMISC_1:def_6;
A8: [!f,x0,x1,x2,x3!] = ((((((f . x0) - (f . x1)) / (- (x1 - x0))) - (((f . x1) - (f . x2)) / (x1 - x2))) / (- (x2 - x0))) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3)
.= ((((- (((f . x0) - (f . x1)) / (x1 - x0))) - (((f . x1) - (f . x2)) / (x1 - x2))) / (- (x2 - x0))) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3) by XCMPLX_1:188
.= (((- ((((f . x0) - (f . x1)) / (x1 - x0)) + (((f . x1) - (f . x2)) / (x1 - x2)))) / (- (x2 - x0))) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3)
.= ((((((f . x0) - (f . x1)) / (x1 - x0)) + (((f . x1) - (f . x2)) / (x1 - x2))) / (x2 - x0)) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3) by XCMPLX_1:191
.= (((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((x1 - x0) * (x1 - x2))) / (x2 - x0)) - (((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x1 - x3))) / (x0 - x3) by A4, A7, XCMPLX_1:116
.= (((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((x1 - x0) * (x1 - x2))) / (x2 - x0)) - ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((x1 - x2) * (x2 - x3))) / (x1 - x3))) / (x0 - x3) by A2, A4, XCMPLX_1:130
.= ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) - ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((x1 - x2) * (x2 - x3))) / (x1 - x3))) / (x0 - x3) by XCMPLX_1:78
.= ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) - (((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3)))) / (x0 - x3) by XCMPLX_1:78
.= (- ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) - (((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))))) / (- (x0 - x3)) by XCMPLX_1:191
.= ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))) - (((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0)))) / (x3 - x0)
.= ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / (((x1 - x2) * (x2 - x3)) * (x1 - x3))) / (x3 - x0)) - ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) / (x3 - x0)) by XCMPLX_1:120
.= (((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x3 - x0))) - ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x1 - x2)) * (x2 - x0))) / (x3 - x0)) by XCMPLX_1:78
.= (((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) / ((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x3 - x0))) - (((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((((x1 - x0) * (x1 - x2)) * (x2 - x0)) * (x3 - x0))) by XCMPLX_1:78
.= ((((((f . x1) - (f . x2)) * (x2 - x3)) - (((f . x2) - (f . x3)) * (x1 - x2))) * (x2 - x0)) / (((((x1 - x2) * (x2 - x3)) * (x1 - x3)) * (x3 - x0)) * (x2 - x0))) - (((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((((x1 - x0) * (x1 - x2)) * (x2 - x0)) * (x3 - x0))) by A6, XCMPLX_1:91
.= (((((((f . x1) - (f . x2)) * (x2 - x3)) * (x2 - x0)) - ((((f . x2) - (f . x3)) * (x1 - x2)) * (x2 - x0))) * (x1 - x0)) / ((((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x0))) - (((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) / ((((x1 - x0) * (x1 - x2)) * (x2 - x0)) * (x3 - x0))) by A7, XCMPLX_1:91
.= (((((((f . x1) - (f . x2)) * (x2 - x3)) * (x2 - x0)) * (x1 - x0)) - (((((f . x2) - (f . x3)) * (x1 - x2)) * (x2 - x0)) * (x1 - x0))) / ((((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x0))) - ((((((f . x0) - (f . x1)) * (x1 - x2)) + (((f . x1) - (f . x2)) * (x1 - x0))) * ((x2 - x3) * (x1 - x3))) / (((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x1 - x0)) * ((x2 - x3) * (x1 - x3)))) by A2, A3, XCMPLX_1:6, XCMPLX_1:91
.= (((((((f . x1) - (f . x2)) * (x2 - x3)) * (x2 - x0)) * (x1 - x0)) - (((((f . x2) - (f . x3)) * (x1 - x2)) * (x2 - x0)) * (x1 - x0))) - ((((((f . x0) - (f . x1)) * (x1 - x2)) * (x2 - x3)) * (x1 - x3)) + (((((f . x1) - (f . x2)) * (x1 - x0)) * (x2 - x3)) * (x1 - x3)))) / ((((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x0)) by XCMPLX_1:120
.= ((((- ((((f . x0) * (x1 - x2)) * (x2 - x3)) * (x1 - x3))) + ((((f . x1) * (x2 - x0)) * (x2 - x3)) * (x3 - x0))) - ((((f . x2) * (x1 - x3)) * (x1 - x0)) * (x3 - x0))) + ((((f . x3) * (x1 - x2)) * (x2 - x0)) * (x1 - x0))) / ((((((x1 - x2) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x0)) ;
A9: [!f,x1,x2,x0,x3!] = ((((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x0)) / (x2 - x0))) / (x1 - x0)) - (((((f . x2) - (f . x0)) / (x2 - x0)) - (((f . x0) - (f . x3)) / (- (x3 - x0)))) / (x2 - x3))) / (x1 - x3)
.= ((((((f . x1) - (f . x2)) / (x1 - x2)) - (((f . x2) - (f . x0)) / (x2 - x0))) / (x1 - x0)) - (((((f . x2) - (f . x0)) / (x2 - x0)) - (- (((f . x0) - (f . x3)) / (x3 - x0)))) / (x2 - x3))) / (x1 - x3) by XCMPLX_1:188
.= (((((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) / ((x1 - x2) * (x2 - x0))) / (x1 - x0)) - (((((f . x2) - (f . x0)) / (x2 - x0)) + (((f . x0) - (f . x3)) / (x3 - x0))) / (x2 - x3))) / (x1 - x3) by A4, A6, XCMPLX_1:130
.= (((((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) / ((x1 - x2) * (x2 - x0))) / (x1 - x0)) - ((((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / ((x3 - x0) * (x2 - x0))) / (x2 - x3))) / (x1 - x3) by A5, A6, XCMPLX_1:116
.= ((((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) / (((x1 - x2) * (x2 - x0)) * (x1 - x0))) - ((((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / ((x3 - x0) * (x2 - x0))) / (x2 - x3))) / (x1 - x3) by XCMPLX_1:78
.= ((((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) / (((x1 - x2) * (x2 - x0)) * (x1 - x0))) - (((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / (((x3 - x0) * (x2 - x0)) * (x2 - x3)))) / (x1 - x3) by XCMPLX_1:78
.= ((((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) / (((x1 - x2) * (x2 - x0)) * (x1 - x0))) / (x1 - x3)) - ((((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / (((x3 - x0) * (x2 - x0)) * (x2 - x3))) / (x1 - x3)) by XCMPLX_1:120
.= (((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) / ((((x1 - x2) * (x2 - x0)) * (x1 - x0)) * (x1 - x3))) - ((((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / (((x3 - x0) * (x2 - x0)) * (x2 - x3))) / (x1 - x3)) by XCMPLX_1:78
.= (((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) / ((((x1 - x2) * (x2 - x0)) * (x1 - x0)) * (x1 - x3))) - (((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / ((((x3 - x0) * (x2 - x0)) * (x2 - x3)) * (x1 - x3))) by XCMPLX_1:78
.= ((((((f . x1) - (f . x2)) * (x2 - x0)) - (((f . x2) - (f . x0)) * (x1 - x2))) * (x3 - x0)) / (((((x1 - x2) * (x2 - x0)) * (x1 - x0)) * (x1 - x3)) * (x3 - x0))) - (((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / ((((x3 - x0) * (x2 - x0)) * (x2 - x3)) * (x1 - x3))) by A5, XCMPLX_1:91
.= (((((((f . x1) - (f . x2)) * (x2 - x0)) * (x3 - x0)) - ((((f . x2) - (f . x0)) * (x1 - x2)) * (x3 - x0))) * (x2 - x3)) / ((((((x1 - x2) * (x2 - x0)) * (x1 - x0)) * (x1 - x3)) * (x3 - x0)) * (x2 - x3))) - (((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) / ((((x3 - x0) * (x2 - x0)) * (x2 - x3)) * (x1 - x3))) by A2, XCMPLX_1:91
.= (((((((f . x1) - (f . x2)) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) - (((((f . x2) - (f . x0)) * (x1 - x2)) * (x3 - x0)) * (x2 - x3))) / ((((((x1 - x2) * (x2 - x0)) * (x1 - x0)) * (x1 - x3)) * (x3 - x0)) * (x2 - x3))) - ((((((f . x2) - (f . x0)) * (x3 - x0)) + (((f . x0) - (f . x3)) * (x2 - x0))) * (x1 - x2)) / (((((x3 - x0) * (x2 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x2))) by A4, XCMPLX_1:91
.= (((((((f . x1) - (f . x2)) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) - (((((f . x2) - (f . x0)) * (x1 - x2)) * (x3 - x0)) * (x2 - x3))) / ((((((x1 - x2) * (x2 - x0)) * (x1 - x0)) * (x1 - x3)) * (x3 - x0)) * (x2 - x3))) - (((((((f . x2) - (f . x0)) * (x3 - x0)) * (x1 - x2)) + ((((f . x0) - (f . x3)) * (x2 - x0)) * (x1 - x2))) * (x1 - x0)) / ((((((x3 - x0) * (x2 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x2)) * (x1 - x0))) by A7, XCMPLX_1:91
.= (((((((f . x1) - (f . x2)) * (x2 - x0)) * (x3 - x0)) * (x2 - x3)) - (((((f . x2) - (f . x0)) * (x1 - x2)) * (x3 - x0)) * (x2 - x3))) - ((((((f . x2) - (f . x0)) * (x3 - x0)) * (x1 - x2)) * (x1 - x0)) + (((((f . x0) - (f . x3)) * (x2 - x0)) * (x1 - x2)) * (x1 - x0)))) / ((((((x3 - x0) * (x2 - x0)) * (x2 - x3)) * (x1 - x3)) * (x1 - x2)) * (x1 - x0)) by XCMPLX_1:120
.= [!f,x0,x1,x2,x3!] by A8 ;
[!f,x1,x0,x2,x3!] = ((((((f . x1) - (f . x0)) / (x1 - x0)) - (- (((f . x0) - (f . x2)) / (x2 - x0)))) / (x1 - x2)) - (((((f . x0) - (f . x2)) / (- (x2 - x0))) - (((f . x2) - (f . x3)) / (x2 - x3))) / (x0 - x3))) / (x1 - x3) by XCMPLX_1:188
.= ((((((f . x1) - (f . x0)) / (x1 - x0)) + (((f . x0) - (f . x2)) / (x2 - x0))) / (x1 - x2)) - (((- (((f . x0) - (f . x2)) / (x2 - x0))) - (((f . x2) - (f . x3)) / (x2 - x3))) / (- (x3 - x0)))) / (x1 - x3) by XCMPLX_1:188
.= ((((((f . x1) - (f . x0)) / (x1 - x0)) + (((f . x0) - (f . x2)) / (x2 - x0))) / (x1 - x2)) - ((- ((((f . x0) - (f . x2)) / (x2 - x0)) + (((f . x2) - (f . x3)) / (x2 - x3)))) / (- (x3 - x0)))) / (x1 - x3)
.= ((((((f . x1) - (f . x0)) / (x1 - x0)) + (((f . x0) - (f . x2)) / (x2 - x0))) / (x1 - x2)) - (((((f . x0) - (f . x2)) / (x2 - x0)) + (((f . x2) - (f . x3)) / (x2 - x3))) / (x3 - x0))) / (x1 - x3) by XCMPLX_1:191
.= (((((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) / ((x2 - x0) * (x1 - x0))) / (x1 - x2)) - (((((f . x0) - (f . x2)) / (x2 - x0)) + (((f . x2) - (f . x3)) / (x2 - x3))) / (x3 - x0))) / (x1 - x3) by A6, A7, XCMPLX_1:116
.= (((((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) / ((x1 - x0) * (x2 - x0))) / (x1 - x2)) - ((((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / ((x2 - x3) * (x2 - x0))) / (x3 - x0))) / (x1 - x3) by A2, A6, XCMPLX_1:116
.= ((((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x2 - x0)) * (x1 - x2))) - ((((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / ((x2 - x3) * (x2 - x0))) / (x3 - x0))) / (x1 - x3) by XCMPLX_1:78
.= ((((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x2 - x0)) * (x1 - x2))) - (((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / (((x2 - x3) * (x2 - x0)) * (x3 - x0)))) / (x1 - x3) by XCMPLX_1:78
.= ((((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) / (((x1 - x0) * (x2 - x0)) * (x1 - x2))) / (x1 - x3)) - ((((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / (((x2 - x3) * (x2 - x0)) * (x3 - x0))) / (x1 - x3)) by XCMPLX_1:120
.= (((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) / ((((x1 - x0) * (x2 - x0)) * (x1 - x2)) * (x1 - x3))) - ((((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / (((x2 - x3) * (x2 - x0)) * (x3 - x0))) / (x1 - x3)) by XCMPLX_1:78
.= (((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) / ((((x1 - x0) * (x2 - x0)) * (x1 - x2)) * (x1 - x3))) - (((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / ((((x2 - x3) * (x2 - x0)) * (x3 - x0)) * (x1 - x3))) by XCMPLX_1:78
.= ((((((f . x1) - (f . x0)) * (x2 - x0)) + (((f . x0) - (f . x2)) * (x1 - x0))) * (x2 - x3)) / (((((x1 - x0) * (x2 - x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3))) - (((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / ((((x2 - x3) * (x2 - x0)) * (x3 - x0)) * (x1 - x3))) by A2, XCMPLX_1:91
.= (((((((f . x1) - (f . x0)) * (x2 - x0)) * (x2 - x3)) + ((((f . x0) - (f . x2)) * (x1 - x0)) * (x2 - x3))) * (x3 - x0)) / ((((((x1 - x0) * (x2 - x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) * (x3 - x0))) - (((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) / ((((x2 - x3) * (x2 - x0)) * (x3 - x0)) * (x1 - x3))) by A5, XCMPLX_1:91
.= (((((((f . x1) - (f . x0)) * (x2 - x0)) * (x2 - x3)) * (x3 - x0)) + (((((f . x0) - (f . x2)) * (x1 - x0)) * (x2 - x3)) * (x3 - x0))) / ((((((x1 - x0) * (x2 - x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) * (x3 - x0))) - ((((((f . x0) - (f . x2)) * (x2 - x3)) + (((f . x2) - (f . x3)) * (x2 - x0))) * (x1 - x0)) / (((((x2 - x3) * (x2 - x0)) * (x3 - x0)) * (x1 - x3)) * (x1 - x0))) by A7, XCMPLX_1:91
.= (((((((f . x1) - (f . x0)) * (x2 - x0)) * (x2 - x3)) * (x3 - x0)) + (((((f . x0) - (f . x2)) * (x1 - x0)) * (x2 - x3)) * (x3 - x0))) / ((((((x1 - x0) * (x2 - x0)) * (x1 - x2)) * (x1 - x3)) * (x2 - x3)) * (x3 - x0))) - (((((((f . x0) - (f . x2)) * (x2 - x3)) * (x1 - x0)) + ((((f . x2) - (f . x3)) * (x2 - x0)) * (x1 - x0))) * (x1 - x2)) / ((((((x2 - x3) * (x2 - x0)) * (x3 - x0)) * (x1 - x3)) * (x1 - x0)) * (x1 - x2))) by A4, XCMPLX_1:91
.= (((((((f . x1) - (f . x0)) * (x2 - x0)) * (x2 - x3)) * (x3 - x0)) + (((((f . x0) - (f . x2)) * (x1 - x0)) * (x2 - x3)) * (x3 - x0))) - ((((((f . x0) - (f . x2)) * (x2 - x3)) * (x1 - x0)) * (x1 - x2)) + (((((f . x2) - (f . x3)) * (x2 - x0)) * (x1 - x0)) * (x1 - x2)))) / ((((((x2 - x3) * (x2 - x0)) * (x3 - x0)) * (x1 - x3)) * (x1 - x0)) * (x1 - x2)) by XCMPLX_1:120
.= [!f,x0,x1,x2,x3!] by A8 ;
hence  ( [!f,x0,x1,x2,x3!] = [!f,x1,x0,x2,x3!] & [!f,x0,x1,x2,x3!] = [!f,x1,x2,x0,x3!] ) by A9; ::_thesis: verum
end;

theorem :: DIFF_2:20
for x0, x1, x2 being Real
for f being Function of REAL,REAL st f is constant holds
[!f,x0,x1,x2!] = 0
proof
let x0, x1, x2 be Real; ::_thesis: for f being Function of REAL,REAL st f is constant holds
[!f,x0,x1,x2!] = 0
let f be Function of REAL,REAL; ::_thesis: ( f is constant implies [!f,x0,x1,x2!] = 0 )
assume A1: f is constant ; ::_thesis: [!f,x0,x1,x2!] = 0
then [!f,x0,x1,x2!] = (0 - [!f,x1,x2!]) / (x0 - x2) by DIFF_1:30
.= (0 - 0) / (x0 - x2) by A1, DIFF_1:30 ;
hence  [!f,x0,x1,x2!] = 0 ; ::_thesis: verum
end;

theorem Th21: :: DIFF_2:21
for x0, x1, a, b being Real st x0 <> x1 holds
[!(AffineMap (a,b)),x0,x1!] = a
proof
let x0, x1, a, b be Real; ::_thesis: ( x0 <> x1 implies [!(AffineMap (a,b)),x0,x1!] = a )
assume  x0 <> x1 ; ::_thesis: [!(AffineMap (a,b)),x0,x1!] = a
then A1: x0 - x1 <> 0 ;
[!(AffineMap (a,b)),x0,x1!] = (((a * x0) + b) - ((AffineMap (a,b)) . x1)) / (x0 - x1) by FCONT_1:def_4
.= (((a * x0) + b) - ((a * x1) + b)) / (x0 - x1) by FCONT_1:def_4
.= (a * (x0 - x1)) / (x0 - x1) ;
hence  [!(AffineMap (a,b)),x0,x1!] = a by A1, XCMPLX_1:89; ::_thesis: verum
end;

theorem Th22: :: DIFF_2:22
for x0, x1, x2, a, b being Real st x0,x1,x2 are_mutually_different holds
[!(AffineMap (a,b)),x0,x1,x2!] = 0
proof
let x0, x1, x2, a, b be Real; ::_thesis: ( x0,x1,x2 are_mutually_different implies [!(AffineMap (a,b)),x0,x1,x2!] = 0 )
assume A1: x0,x1,x2 are_mutually_different ; ::_thesis: [!(AffineMap (a,b)),x0,x1,x2!] = 0
then A2: x1 <> x2 by ZFMISC_1:def_5;
 x0 <> x1 by A1, ZFMISC_1:def_5;
then [!(AffineMap (a,b)),x0,x1,x2!] = (a - [!(AffineMap (a,b)),x1,x2!]) / (x0 - x2) by Th21
.= (a - a) / (x0 - x2) by A2, Th21 ;
hence  [!(AffineMap (a,b)),x0,x1,x2!] = 0 ; ::_thesis: verum
end;

theorem :: DIFF_2:23
for x0, x1, x2, x3, a, b being Real st x0,x1,x2,x3 are_mutually_different holds
[!(AffineMap (a,b)),x0,x1,x2,x3!] = 0
proof
let x0, x1, x2, x3, a, b be Real; ::_thesis: ( x0,x1,x2,x3 are_mutually_different implies [!(AffineMap (a,b)),x0,x1,x2,x3!] = 0 )
assume A1: x0,x1,x2,x3 are_mutually_different ; ::_thesis: [!(AffineMap (a,b)),x0,x1,x2,x3!] = 0
then A2: x1 <> x2 by ZFMISC_1:def_6;
 ( x1 <> x3 & x2 <> x3 ) by A1, ZFMISC_1:def_6;
then A3: x1,x2,x3 are_mutually_different by A2, ZFMISC_1:def_5;
 ( x0 <> x1 & x0 <> x2 ) by A1, ZFMISC_1:def_6;
then  x0,x1,x2 are_mutually_different by A2, ZFMISC_1:def_5;
then [!(AffineMap (a,b)),x0,x1,x2,x3!] = (0 - [!(AffineMap (a,b)),x1,x2,x3!]) / (x0 - x3) by Th22
.= (0 - 0) / (x0 - x3) by A3, Th22 ;
hence  [!(AffineMap (a,b)),x0,x1,x2,x3!] = 0 ; ::_thesis: verum
end;

theorem :: DIFF_2:24
for a, b, h, x being Real holds (fD ((AffineMap (a,b)),h)) . x = a * h
proof
let a, b, h, x be Real; ::_thesis: (fD ((AffineMap (a,b)),h)) . x = a * h
(fD ((AffineMap (a,b)),h)) . x = ((AffineMap (a,b)) . (x + h)) - ((AffineMap (a,b)) . x) by DIFF_1:3
.= ((a * (x + h)) + b) - ((AffineMap (a,b)) . x) by FCONT_1:def_4
.= (((a * x) + (a * h)) + b) - ((a * x) + b) by FCONT_1:def_4 ;
hence  (fD ((AffineMap (a,b)),h)) . x = a * h ; ::_thesis: verum
end;

theorem :: DIFF_2:25
for a, b, h, x being Real holds (bD ((AffineMap (a,b)),h)) . x = a * h
proof
let a, b, h, x be Real; ::_thesis: (bD ((AffineMap (a,b)),h)) . x = a * h
(bD ((AffineMap (a,b)),h)) . x = ((AffineMap (a,b)) . x) - ((AffineMap (a,b)) . (x - h)) by DIFF_1:4
.= ((a * x) + b) - ((AffineMap (a,b)) . (x - h)) by FCONT_1:def_4
.= ((a * x) + b) - ((a * (x - h)) + b) by FCONT_1:def_4 ;
hence  (bD ((AffineMap (a,b)),h)) . x = a * h ; ::_thesis: verum
end;

theorem :: DIFF_2:26
for a, b, h, x being Real holds (cD ((AffineMap (a,b)),h)) . x = a * h
proof
let a, b, h, x be Real; ::_thesis: (cD ((AffineMap (a,b)),h)) . x = a * h
(cD ((AffineMap (a,b)),h)) . x = ((AffineMap (a,b)) . (x + (h / 2))) - ((AffineMap (a,b)) . (x - (h / 2))) by DIFF_1:5
.= ((a * (x + (h / 2))) + b) - ((AffineMap (a,b)) . (x - (h / 2))) by FCONT_1:def_4
.= ((a * (x + (h / 2))) + b) - ((a * (x - (h / 2))) + b) by FCONT_1:def_4 ;
hence  (cD ((AffineMap (a,b)),h)) . x = a * h ; ::_thesis: verum
end;

theorem Th27: :: DIFF_2:27
for a, b, c, x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0 <> x1 holds
[!f,x0,x1!] = (a * (x0 + x1)) + b
proof
let a, b, c, x0, x1 be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0 <> x1 holds
[!f,x0,x1!] = (a * (x0 + x1)) + b
let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0 <> x1 implies [!f,x0,x1!] = (a * (x0 + x1)) + b )
assume that
A1: for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c and
A2: x0 <> x1 ; ::_thesis: [!f,x0,x1!] = (a * (x0 + x1)) + b
A3: x0 - x1 <> 0 by A2;
[!f,x0,x1!] = ((((a * (x0 ^2)) + (b * x0)) + c) - (f . x1)) / (x0 - x1) by A1
.= ((((a * (x0 ^2)) + (b * x0)) + c) - (((a * (x1 ^2)) + (b * x1)) + c)) / (x0 - x1) by A1
.= (((a * (x0 + x1)) + b) * (x0 - x1)) / (x0 - x1) ;
hence  [!f,x0,x1!] = (a * (x0 + x1)) + b by A3, XCMPLX_1:89; ::_thesis: verum
end;

theorem Th28: :: DIFF_2:28
for a, b, c, x0, x1, x2 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0,x1,x2 are_mutually_different holds
[!f,x0,x1,x2!] = a
proof
let a, b, c, x0, x1, x2 be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0,x1,x2 are_mutually_different holds
[!f,x0,x1,x2!] = a
let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0,x1,x2 are_mutually_different implies [!f,x0,x1,x2!] = a )
assume A1: for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ; ::_thesis: ( not x0,x1,x2 are_mutually_different or [!f,x0,x1,x2!] = a )
assume A2: x0,x1,x2 are_mutually_different ; ::_thesis: [!f,x0,x1,x2!] = a
then A3: x1 <> x2 by ZFMISC_1:def_5;
A4: x0 - x2 <> 0 by A2, ZFMISC_1:def_5;
 x0 <> x1 by A2, ZFMISC_1:def_5;
then [!f,x0,x1,x2!] = (((a * (x0 + x1)) + b) - [!f,x1,x2!]) / (x0 - x2) by A1, Th27
.= (((a * (x0 + x1)) + b) - ((a * (x1 + x2)) + b)) / (x0 - x2) by A1, A3, Th27
.= (a * (x0 - x2)) / (x0 - x2) ;
hence  [!f,x0,x1,x2!] = a by A4, XCMPLX_1:89; ::_thesis: verum
end;

theorem Th29: :: DIFF_2:29
for a, b, c, x0, x1, x2, x3 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0,x1,x2,x3 are_mutually_different holds
[!f,x0,x1,x2,x3!] = 0
proof
let a, b, c, x0, x1, x2, x3 be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0,x1,x2,x3 are_mutually_different holds
[!f,x0,x1,x2,x3!] = 0
let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0,x1,x2,x3 are_mutually_different implies [!f,x0,x1,x2,x3!] = 0 )
assume A1: for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ; ::_thesis: ( not x0,x1,x2,x3 are_mutually_different or [!f,x0,x1,x2,x3!] = 0 )
assume A2: x0,x1,x2,x3 are_mutually_different ; ::_thesis: [!f,x0,x1,x2,x3!] = 0
then A3: x1 <> x2 by ZFMISC_1:def_6;
 ( x1 <> x3 & x2 <> x3 ) by A2, ZFMISC_1:def_6;
then A4: x1,x2,x3 are_mutually_different by A3, ZFMISC_1:def_5;
 ( x0 <> x1 & x0 <> x2 ) by A2, ZFMISC_1:def_6;
then  x0,x1,x2 are_mutually_different by A3, ZFMISC_1:def_5;
then [!f,x0,x1,x2,x3!] = (a - [!f,x1,x2,x3!]) / (x0 - x3) by A1, Th28
.= (a - a) / (x0 - x3) by A1, A4, Th28 ;
hence  [!f,x0,x1,x2,x3!] = 0 ; ::_thesis: verum
end;

theorem :: DIFF_2:30
for a, b, c, x0, x1, x2, x3, x4 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0,x1,x2,x3,x4 are_mutually_different holds
[!f,x0,x1,x2,x3,x4!] = 0
proof
let a, b, c, x0, x1, x2, x3, x4 be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0,x1,x2,x3,x4 are_mutually_different holds
[!f,x0,x1,x2,x3,x4!] = 0
let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) & x0,x1,x2,x3,x4 are_mutually_different implies [!f,x0,x1,x2,x3,x4!] = 0 )
assume A1: for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ; ::_thesis: ( not x0,x1,x2,x3,x4 are_mutually_different or [!f,x0,x1,x2,x3,x4!] = 0 )
assume A2: x0,x1,x2,x3,x4 are_mutually_different ; ::_thesis: [!f,x0,x1,x2,x3,x4!] = 0
then A3: ( x1 <> x2 & x1 <> x3 ) by ZFMISC_1:def_7;
A4: x0 <> x3 by A2, ZFMISC_1:def_7;
A5: x2 <> x3 by A2, ZFMISC_1:def_7;
A6: x3 <> x4 by A2, ZFMISC_1:def_7;
 ( x1 <> x4 & x2 <> x4 ) by A2, ZFMISC_1:def_7;
then A7: x1,x2,x3,x4 are_mutually_different by A3, A5, A6, ZFMISC_1:def_6;
 ( x0 <> x1 & x0 <> x2 ) by A2, ZFMISC_1:def_7;
then  x0,x1,x2,x3 are_mutually_different by A4, A3, A5, ZFMISC_1:def_6;
then [!f,x0,x1,x2,x3,x4!] = (0 - [!f,x1,x2,x3,x4!]) / (x0 - x4) by A1, Th29
.= (0 - 0) / (x0 - x4) by A1, A7, Th29 ;
hence  [!f,x0,x1,x2,x3,x4!] = 0 ; ::_thesis: verum
end;

theorem :: DIFF_2:31
for a, b, c, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) holds
for x being Real holds (fD (f,h)) . x = ((((2 * a) * h) * x) + (a * (h ^2))) + (b * h)
proof
let a, b, c, h be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) holds
for x being Real holds (fD (f,h)) . x = ((((2 * a) * h) * x) + (a * (h ^2))) + (b * h)
let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) implies for x being Real holds (fD (f,h)) . x = ((((2 * a) * h) * x) + (a * (h ^2))) + (b * h) )
assume A1: for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ; ::_thesis: for x being Real holds (fD (f,h)) . x = ((((2 * a) * h) * x) + (a * (h ^2))) + (b * h)
let x be Real; ::_thesis: (fD (f,h)) . x = ((((2 * a) * h) * x) + (a * (h ^2))) + (b * h)
(fD (f,h)) . x = (f . (x + h)) - (f . x) by DIFF_1:3
.= (((a * ((x + h) ^2)) + (b * (x + h))) + c) - (f . x) by A1
.= (((a * ((x + h) ^2)) + (b * (x + h))) + c) - (((a * (x ^2)) + (b * x)) + c) by A1
.= ((((2 * a) * h) * x) + (a * (h ^2))) + (b * h) ;
hence  (fD (f,h)) . x = ((((2 * a) * h) * x) + (a * (h ^2))) + (b * h) ; ::_thesis: verum
end;

theorem :: DIFF_2:32
for a, b, c, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) holds
for x being Real holds (bD (f,h)) . x = ((((2 * a) * h) * x) - (a * (h ^2))) + (b * h)
proof
let a, b, c, h be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) holds
for x being Real holds (bD (f,h)) . x = ((((2 * a) * h) * x) - (a * (h ^2))) + (b * h)
let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) implies for x being Real holds (bD (f,h)) . x = ((((2 * a) * h) * x) - (a * (h ^2))) + (b * h) )
assume A1: for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ; ::_thesis: for x being Real holds (bD (f,h)) . x = ((((2 * a) * h) * x) - (a * (h ^2))) + (b * h)
let x be Real; ::_thesis: (bD (f,h)) . x = ((((2 * a) * h) * x) - (a * (h ^2))) + (b * h)
(bD (f,h)) . x = (f . x) - (f . (x - h)) by DIFF_1:4
.= (((a * (x ^2)) + (b * x)) + c) - (f . (x - h)) by A1
.= (((a * (x ^2)) + (b * x)) + c) - (((a * ((x - h) ^2)) + (b * (x - h))) + c) by A1
.= ((((2 * a) * h) * x) - (a * (h ^2))) + (b * h) ;
hence  (bD (f,h)) . x = ((((2 * a) * h) * x) - (a * (h ^2))) + (b * h) ; ::_thesis: verum
end;

theorem :: DIFF_2:33
for a, b, c, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) holds
for x being Real holds (cD (f,h)) . x = (((2 * a) * h) * x) + (b * h)
proof
let a, b, c, h be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) holds
for x being Real holds (cD (f,h)) . x = (((2 * a) * h) * x) + (b * h)
let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) implies for x being Real holds (cD (f,h)) . x = (((2 * a) * h) * x) + (b * h) )
assume A1: for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ; ::_thesis: for x being Real holds (cD (f,h)) . x = (((2 * a) * h) * x) + (b * h)
let x be Real; ::_thesis: (cD (f,h)) . x = (((2 * a) * h) * x) + (b * h)
(cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2))) by DIFF_1:5
.= (((a * ((x + (h / 2)) ^2)) + (b * (x + (h / 2)))) + c) - (f . (x - (h / 2))) by A1
.= (((a * ((x + (h / 2)) ^2)) + (b * (x + (h / 2)))) + c) - (((a * ((x - (h / 2)) ^2)) + (b * (x - (h / 2)))) + c) by A1
.= (((2 * a) * h) * x) + (b * h) ;
hence  (cD (f,h)) . x = (((2 * a) * h) * x) + (b * h) ; ::_thesis: verum
end;

theorem Th34: :: DIFF_2:34
for k, x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = k / x ) & x0 <> x1 & x0 <> 0 & x1 <> 0 holds
[!f,x0,x1!] = - (k / (x0 * x1))
proof
let k, x0, x1 be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = k / x ) & x0 <> x1 & x0 <> 0 & x1 <> 0 holds
[!f,x0,x1!] = - (k / (x0 * x1))
let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = k / x ) & x0 <> x1 & x0 <> 0 & x1 <> 0 implies [!f,x0,x1!] = - (k / (x0 * x1)) )
assume that
A1: for x being Real holds f . x = k / x and
A2: x0 <> x1 and
A3: x0 <> 0 and
A4: x1 <> 0 ; ::_thesis: [!f,x0,x1!] = - (k / (x0 * x1))
A5: x1 - x0 <> 0 by A2;
[!f,x0,x1!] = ((k / x0) - (f . x1)) / (x0 - x1) by A1
.= ((k / x0) - (k / x1)) / (x0 - x1) by A1
.= (((k * x1) / (x0 * x1)) - (k / x1)) / (x0 - x1) by A4, XCMPLX_1:91
.= (((k * x1) / (x0 * x1)) - ((k * x0) / (x0 * x1))) / (x0 - x1) by A3, XCMPLX_1:91
.= (((k * x1) - (k * x0)) / (x0 * x1)) / (x0 - x1) by XCMPLX_1:120
.= ((k * (x1 - x0)) / (x0 * x1)) / (- (x1 - x0))
.= - (((k * (x1 - x0)) / (x0 * x1)) / (x1 - x0)) by XCMPLX_1:188
.= - (((k * (x1 - x0)) / (x1 - x0)) / (x0 * x1)) by XCMPLX_1:48 ;
hence  [!f,x0,x1!] = - (k / (x0 * x1)) by A5, XCMPLX_1:89; ::_thesis: verum
end;

theorem Th35: :: DIFF_2:35
for k, x0, x1, x2 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = k / x ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x0,x1,x2 are_mutually_different holds
[!f,x0,x1,x2!] = k / ((x0 * x1) * x2)
proof
let k, x0, x1, x2 be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = k / x ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x0,x1,x2 are_mutually_different holds
[!f,x0,x1,x2!] = k / ((x0 * x1) * x2)
let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = k / x ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x0,x1,x2 are_mutually_different implies [!f,x0,x1,x2!] = k / ((x0 * x1) * x2) )
assume that
A1: for x being Real holds f . x = k / x and
A2: x0 <> 0 and
A3: x1 <> 0 and
A4: x2 <> 0 ; ::_thesis: ( not x0,x1,x2 are_mutually_different or [!f,x0,x1,x2!] = k / ((x0 * x1) * x2) )
assume A5: x0,x1,x2 are_mutually_different ; ::_thesis: [!f,x0,x1,x2!] = k / ((x0 * x1) * x2)
then A6: x1 <> x2 by ZFMISC_1:def_5;
A7: x0 - x2 <> 0 by A5, ZFMISC_1:def_5;
 x0 <> x1 by A5, ZFMISC_1:def_5;
then [!f,x0,x1,x2!] = ((- (k / (x0 * x1))) - [!f,x1,x2!]) / (x0 - x2) by A1, A2, A3, Th34
.= ((- (k / (x0 * x1))) - (- (k / (x1 * x2)))) / (x0 - x2) by A1, A3, A4, A6, Th34
.= ((- (k / (x0 * x1))) + (k / (x1 * x2))) / (x0 - x2)
.= ((- ((k * x2) / ((x0 * x1) * x2))) + (k / (x1 * x2))) / (x0 - x2) by A4, XCMPLX_1:91
.= ((- ((k * x2) / ((x0 * x1) * x2))) + ((k * x0) / (x0 * (x1 * x2)))) / (x0 - x2) by A2, XCMPLX_1:91
.= (- (((k * x2) / ((x0 * x1) * x2)) - ((k * x0) / ((x0 * x1) * x2)))) / (x0 - x2)
.= (- (((k * x2) - (k * x0)) / ((x0 * x1) * x2))) / (x0 - x2) by XCMPLX_1:120
.= ((- (k * (x2 - x0))) / ((x0 * x1) * x2)) / (x0 - x2) by XCMPLX_1:187
.= (k * (x0 - x2)) / (((x0 * x1) * x2) * (x0 - x2)) by XCMPLX_1:78 ;
hence  [!f,x0,x1,x2!] = k / ((x0 * x1) * x2) by A7, XCMPLX_1:91; ::_thesis: verum
end;

theorem Th36: :: DIFF_2:36
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 ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 & x0,x1,x2,x3 are_mutually_different holds
[!f,x0,x1,x2,x3!] = - (k / (((x0 * x1) * x2) * 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 ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 & x0,x1,x2,x3 are_mutually_different holds
[!f,x0,x1,x2,x3!] = - (k / (((x0 * x1) * x2) * x3))
let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = k / x ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 & x0,x1,x2,x3 are_mutually_different implies [!f,x0,x1,x2,x3!] = - (k / (((x0 * x1) * x2) * x3)) )
assume that
A1: for x being Real holds f . x = k / x and
A2: x0 <> 0 and
A3: ( x1 <> 0 & x2 <> 0 ) and
A4: x3 <> 0 ; ::_thesis: ( not x0,x1,x2,x3 are_mutually_different or [!f,x0,x1,x2,x3!] = - (k / (((x0 * x1) * x2) * x3)) )
assume A5: x0,x1,x2,x3 are_mutually_different ; ::_thesis: [!f,x0,x1,x2,x3!] = - (k / (((x0 * x1) * x2) * x3))
then A6: x1 <> x2 by ZFMISC_1:def_6;
 ( x1 <> x3 & x2 <> x3 ) by A5, ZFMISC_1:def_6;
then A7: x1,x2,x3 are_mutually_different by A6, ZFMISC_1:def_5;
A8: x0 - x3 <> 0 by A5, ZFMISC_1:def_6;
 ( x0 <> x1 & x0 <> x2 ) by A5, ZFMISC_1:def_6;
then  x0,x1,x2 are_mutually_different by A6, ZFMISC_1:def_5;
then [!f,x0,x1,x2,x3!] = ((k / ((x0 * x1) * x2)) - [!f,x1,x2,x3!]) / (x0 - x3) by A1, A2, A3, Th35
.= ((k / ((x0 * x1) * x2)) - (k / ((x1 * x2) * x3))) / (x0 - x3) by A1, A3, A4, A7, Th35
.= (((k * x3) / (((x0 * x1) * x2) * x3)) - (k / ((x1 * x2) * x3))) / (x0 - x3) by A4, XCMPLX_1:91
.= (((k * x3) / (((x0 * x1) * x2) * x3)) - ((k * x0) / (x0 * ((x1 * x2) * x3)))) / (x0 - x3) by A2, XCMPLX_1:91
.= (((k * x3) - (k * x0)) / (((x0 * x1) * x2) * x3)) / (x0 - x3) by XCMPLX_1:120
.= ((- k) * (x0 - x3)) / ((((x0 * x1) * x2) * x3) * (x0 - x3)) by XCMPLX_1:78
.= (- k) / (((x0 * x1) * x2) * x3) by A8, XCMPLX_1:91 ;
hence  [!f,x0,x1,x2,x3!] = - (k / (((x0 * x1) * x2) * x3)) by XCMPLX_1:187; ::_thesis: verum
end;

theorem :: DIFF_2:37
for k, x0, x1, x2, x3, x4 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = k / x ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 & x4 <> 0 & x0,x1,x2,x3,x4 are_mutually_different holds
[!f,x0,x1,x2,x3,x4!] = k / ((((x0 * x1) * x2) * x3) * x4)
proof
let k, x0, x1, x2, x3, x4 be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = k / x ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 & x4 <> 0 & x0,x1,x2,x3,x4 are_mutually_different holds
[!f,x0,x1,x2,x3,x4!] = k / ((((x0 * x1) * x2) * x3) * x4)
let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f . x = k / x ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 & x4 <> 0 & x0,x1,x2,x3,x4 are_mutually_different implies [!f,x0,x1,x2,x3,x4!] = k / ((((x0 * x1) * x2) * x3) * x4) )
assume that
A1: for x being Real holds f . x = k / x and
A2: x0 <> 0 and
A3: ( x1 <> 0 & x2 <> 0 & x3 <> 0 ) and
A4: x4 <> 0 ; ::_thesis: ( not x0,x1,x2,x3,x4 are_mutually_different or [!f,x0,x1,x2,x3,x4!] = k / ((((x0 * x1) * x2) * x3) * x4) )
assume A5: x0,x1,x2,x3,x4 are_mutually_different ; ::_thesis: [!f,x0,x1,x2,x3,x4!] = k / ((((x0 * x1) * x2) * x3) * x4)
then A6: ( x1 <> x2 & x1 <> x3 ) by ZFMISC_1:def_7;
A7: x3 <> x4 by A5, ZFMISC_1:def_7;
A8: x2 <> x3 by A5, ZFMISC_1:def_7;
A9: x0 - x4 <> 0 by A5, ZFMISC_1:def_7;
A10: x0 <> x3 by A5, ZFMISC_1:def_7;
 ( x1 <> x4 & x2 <> x4 ) by A5, ZFMISC_1:def_7;
then A11: x1,x2,x3,x4 are_mutually_different by A6, A8, A7, ZFMISC_1:def_6;
 ( x0 <> x1 & x0 <> x2 ) by A5, ZFMISC_1:def_7;
then  x0,x1,x2,x3 are_mutually_different by A10, A6, A8, ZFMISC_1:def_6;
then [!f,x0,x1,x2,x3,x4!] = ((- (k / (((x0 * x1) * x2) * x3))) - [!f,x1,x2,x3,x4!]) / (x0 - x4) by A1, A2, A3, Th36
.= ((- (k / (((x0 * x1) * x2) * x3))) - (- (k / (((x1 * x2) * x3) * x4)))) / (x0 - x4) by A1, A3, A4, A11, Th36
.= ((- (k / (((x0 * x1) * x2) * x3))) + (k / (((x1 * x2) * x3) * x4))) / (x0 - x4)
.= ((- ((k * x4) / ((((x0 * x1) * x2) * x3) * x4))) + (k / (((x1 * x2) * x3) * x4))) / (x0 - x4) by A4, XCMPLX_1:91
.= ((- ((k * x4) / ((((x0 * x1) * x2) * x3) * x4))) + ((k * x0) / (x0 * (((x1 * x2) * x3) * x4)))) / (x0 - x4) by A2, XCMPLX_1:91
.= (((k * x0) / ((((x0 * x1) * x2) * x3) * x4)) - ((k * x4) / ((((x0 * x1) * x2) * x3) * x4))) / (x0 - x4)
.= (((k * x0) - (k * x4)) / ((((x0 * x1) * x2) * x3) * x4)) / (x0 - x4) by XCMPLX_1:120
.= (k * (x0 - x4)) / (((((x0 * x1) * x2) * x3) * x4) * (x0 - x4)) by XCMPLX_1:78 ;
hence  [!f,x0,x1,x2,x3,x4!] = k / ((((x0 * x1) * x2) * x3) * x4) by A9, XCMPLX_1:91; ::_thesis: verum
end;

theorem :: DIFF_2:38
for k, h being Real
for f being Function of REAL,REAL st ( for x being Real holds
( f . x = k / x & x <> 0 & x + h <> 0 ) ) holds
for x being Real holds (fD (f,h)) . x = (- (k * h)) / ((x + h) * x) ;

theorem :: DIFF_2:39
for k, h being Real
for f being Function of REAL,REAL st ( for x being Real holds
( f . x = k / x & x <> 0 & x - h <> 0 ) ) holds
for x being Real holds (bD (f,h)) . x = (- (k * h)) / ((x - h) * x) ;

theorem :: DIFF_2:40
for k, h being Real
for f being Function of REAL,REAL st ( for x being Real holds
( f . x = k / x & x + (h / 2) <> 0 & x - (h / 2) <> 0 ) ) holds
for x being Real holds (cD (f,h)) . x = (- (k * h)) / ((x - (h / 2)) * (x + (h / 2)))
proof
let k, h be Real; ::_thesis: for f being Function of REAL,REAL st ( for x being Real holds
( f . x = k / x & x + (h / 2) <> 0 & x - (h / 2) <> 0 ) ) holds
for x being Real holds (cD (f,h)) . x = (- (k * h)) / ((x - (h / 2)) * (x + (h / 2)))
let f be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds
( f . x = k / x & x + (h / 2) <> 0 & x - (h / 2) <> 0 ) ) implies for x being Real holds (cD (f,h)) . x = (- (k * h)) / ((x - (h / 2)) * (x + (h / 2))) )
assume A1: for x being Real holds
( f . x = k / x & x + (h / 2) <> 0 & x - (h / 2) <> 0 ) ; ::_thesis: for x being Real holds (cD (f,h)) . x = (- (k * h)) / ((x - (h / 2)) * (x + (h / 2)))
let x be Real; ::_thesis: (cD (f,h)) . x = (- (k * h)) / ((x - (h / 2)) * (x + (h / 2)))
A2: x + (h / 2) <> 0 by A1;
A3: x - (h / 2) <> 0 by A1;
(cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2))) by DIFF_1:5
.= (k / (x + (h / 2))) - (f . (x - (h / 2))) by A1
.= (k / (x + (h / 2))) - (k / (x - (h / 2))) by A1
.= ((k * (x - (h / 2))) / ((x - (h / 2)) * (x + (h / 2)))) - (k / (x - (h / 2))) by A3, XCMPLX_1:91
.= ((k * (x - (h / 2))) / ((x - (h / 2)) * (x + (h / 2)))) - ((k * (x + (h / 2))) / ((x - (h / 2)) * (x + (h / 2)))) by A2, XCMPLX_1:91
.= (((k * x) - (k * (h / 2))) - (k * (x + (h / 2)))) / ((x - (h / 2)) * (x + (h / 2))) by XCMPLX_1:120 ;
hence  (cD (f,h)) . x = (- (k * h)) / ((x - (h / 2)) * (x + (h / 2))) ; ::_thesis: verum
end;

theorem :: DIFF_2:41
for x0, x1 being Real holds [!sin,x0,x1!] = ((2 * (cos ((x0 + x1) / 2))) * (sin ((x0 - x1) / 2))) / (x0 - x1)
proof
let x0, x1 be Real; ::_thesis: [!sin,x0,x1!] = ((2 * (cos ((x0 + x1) / 2))) * (sin ((x0 - x1) / 2))) / (x0 - x1)
[!sin,x0,x1!] = ((sin x0) - (sin x1)) / (x0 - x1)
.= (2 * ((cos ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2)))) / (x0 - x1) by SIN_COS4:16 ;
hence  [!sin,x0,x1!] = ((2 * (cos ((x0 + x1) / 2))) * (sin ((x0 - x1) / 2))) / (x0 - x1) ; ::_thesis: verum
end;

theorem :: DIFF_2:42
for h, x being Real holds (fD (sin,h)) . x = 2 * ((cos (((2 * x) + h) / 2)) * (sin (h / 2)))
proof
let h, x be Real; ::_thesis: (fD (sin,h)) . x = 2 * ((cos (((2 * x) + h) / 2)) * (sin (h / 2)))
(fD (sin,h)) . x = (sin (x + h)) - (sin x) by DIFF_1:3
.= 2 * ((cos ((x + (h + x)) / 2)) * (sin (((x + h) - x) / 2))) by SIN_COS4:16 ;
hence  (fD (sin,h)) . x = 2 * ((cos (((2 * x) + h) / 2)) * (sin (h / 2))) ; ::_thesis: verum
end;

theorem :: DIFF_2:43
for h, x being Real holds (bD (sin,h)) . x = 2 * ((cos (((2 * x) - h) / 2)) * (sin (h / 2)))
proof
let h, x be Real; ::_thesis: (bD (sin,h)) . x = 2 * ((cos (((2 * x) - h) / 2)) * (sin (h / 2)))
(bD (sin,h)) . x = (sin x) - (sin (x - h)) by DIFF_1:4
.= 2 * ((cos ((x + (x - h)) / 2)) * (sin ((x - (x - h)) / 2))) by SIN_COS4:16 ;
hence  (bD (sin,h)) . x = 2 * ((cos (((2 * x) - h) / 2)) * (sin (h / 2))) ; ::_thesis: verum
end;

theorem :: DIFF_2:44
for h, x being Real holds (cD (sin,h)) . x = 2 * ((cos x) * (sin (h / 2)))
proof
let h, x be Real; ::_thesis: (cD (sin,h)) . x = 2 * ((cos x) * (sin (h / 2)))
(cD (sin,h)) . x = (sin (x + (h / 2))) - (sin (x - (h / 2))) by DIFF_1:5
.= 2 * ((cos (((x + (h / 2)) + (x - (h / 2))) / 2)) * (sin (((x + (h / 2)) - (x - (h / 2))) / 2))) by SIN_COS4:16 ;
hence  (cD (sin,h)) . x = 2 * ((cos x) * (sin (h / 2))) ; ::_thesis: verum
end;

theorem :: DIFF_2:45
for x0, x1 being Real holds [!cos,x0,x1!] = - (((2 * (sin ((x0 + x1) / 2))) * (sin ((x0 - x1) / 2))) / (x0 - x1))
proof
let x0, x1 be Real; ::_thesis: [!cos,x0,x1!] = - (((2 * (sin ((x0 + x1) / 2))) * (sin ((x0 - x1) / 2))) / (x0 - x1))
[!cos,x0,x1!] = ((cos x0) - (cos x1)) / (x0 - x1)
.= (- (2 * ((sin ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2))))) / (x0 - x1) by SIN_COS4:18 ;
hence  [!cos,x0,x1!] = - (((2 * (sin ((x0 + x1) / 2))) * (sin ((x0 - x1) / 2))) / (x0 - x1)) by XCMPLX_1:187; ::_thesis: verum
end;

theorem :: DIFF_2:46
for h, x being Real holds (fD (cos,h)) . x = - (2 * ((sin (((2 * x) + h) / 2)) * (sin (h / 2))))
proof
let h, x be Real; ::_thesis: (fD (cos,h)) . x = - (2 * ((sin (((2 * x) + h) / 2)) * (sin (h / 2))))
(fD (cos,h)) . x = (cos (x + h)) - (cos x) by DIFF_1:3
.= - (2 * ((sin ((x + (x + h)) / 2)) * (sin (((x + h) - x) / 2)))) by SIN_COS4:18 ;
hence  (fD (cos,h)) . x = - (2 * ((sin (((2 * x) + h) / 2)) * (sin (h / 2)))) ; ::_thesis: verum
end;

theorem :: DIFF_2:47
for h, x being Real holds (bD (cos,h)) . x = - (2 * ((sin (((2 * x) - h) / 2)) * (sin (h / 2))))
proof
let h, x be Real; ::_thesis: (bD (cos,h)) . x = - (2 * ((sin (((2 * x) - h) / 2)) * (sin (h / 2))))
(bD (cos,h)) . x = (cos x) - (cos (x - h)) by DIFF_1:4
.= - (2 * ((sin ((x + (x - h)) / 2)) * (sin ((x - (x - h)) / 2)))) by SIN_COS4:18 ;
hence  (bD (cos,h)) . x = - (2 * ((sin (((2 * x) - h) / 2)) * (sin (h / 2)))) ; ::_thesis: verum
end;

theorem :: DIFF_2:48
for h, x being Real holds (cD (cos,h)) . x = - (2 * ((sin x) * (sin (h / 2))))
proof
let h, x be Real; ::_thesis: (cD (cos,h)) . x = - (2 * ((sin x) * (sin (h / 2))))
(cD (cos,h)) . x = (cos (x + (h / 2))) - (cos (x - (h / 2))) by DIFF_1:5
.= - (2 * ((sin (((x + (h / 2)) + (x - (h / 2))) / 2)) * (sin (((x + (h / 2)) - (x - (h / 2))) / 2)))) by SIN_COS4:18 ;
hence  (cD (cos,h)) . x = - (2 * ((sin x) * (sin (h / 2)))) ; ::_thesis: verum
end;

theorem :: DIFF_2:49
for x0, x1 being Real holds [!(sin (#) sin),x0,x1!] = ((1 / 2) * ((cos (2 * x1)) - (cos (2 * x0)))) / (x0 - x1)
proof
let x0, x1 be Real; ::_thesis: [!(sin (#) sin),x0,x1!] = ((1 / 2) * ((cos (2 * x1)) - (cos (2 * x0)))) / (x0 - x1)
[!(sin (#) sin),x0,x1!] = (((sin . x0) * (sin . x0)) - ((sin (#) sin) . x1)) / (x0 - x1) by VALUED_1:5
.= (((sin x0) * (sin x0)) - ((sin x1) * (sin x1))) / (x0 - x1) by VALUED_1:5
.= ((- ((1 / 2) * ((cos (x0 + x0)) - (cos (x0 - x0))))) - ((sin x1) * (sin x1))) / (x0 - x1) by SIN_COS4:29
.= ((- ((1 / 2) * ((cos (x0 + x0)) - (cos (x0 - x0))))) - (- ((1 / 2) * ((cos (x1 + x1)) - (cos (x1 - x1)))))) / (x0 - x1) by SIN_COS4:29
.= ((1 / 2) * ((cos (2 * x1)) - (cos (2 * x0)))) / (x0 - x1) ;
hence  [!(sin (#) sin),x0,x1!] = ((1 / 2) * ((cos (2 * x1)) - (cos (2 * x0)))) / (x0 - x1) ; ::_thesis: verum
end;

theorem :: DIFF_2:50
for h, x being Real holds (fD ((sin (#) sin),h)) . x = (1 / 2) * ((cos (2 * x)) - (cos (2 * (x + h))))
proof
let h, x be Real; ::_thesis: (fD ((sin (#) sin),h)) . x = (1 / 2) * ((cos (2 * x)) - (cos (2 * (x + h))))
(fD ((sin (#) sin),h)) . x = ((sin (#) sin) . (x + h)) - ((sin (#) sin) . x) by DIFF_1:3
.= ((sin . (x + h)) * (sin . (x + h))) - ((sin (#) sin) . x) by VALUED_1:5
.= ((sin (x + h)) * (sin (x + h))) - ((sin x) * (sin x)) by VALUED_1:5
.= (- ((1 / 2) * ((cos ((x + h) + (x + h))) - (cos ((x + h) - (x + h)))))) - ((sin x) * (sin x)) by SIN_COS4:29
.= (- ((1 / 2) * ((cos (2 * (x + h))) - (cos 0)))) - (- ((1 / 2) * ((cos (x + x)) - (cos (x - x))))) by SIN_COS4:29 ;
hence  (fD ((sin (#) sin),h)) . x = (1 / 2) * ((cos (2 * x)) - (cos (2 * (x + h)))) ; ::_thesis: verum
end;

theorem :: DIFF_2:51
for h, x being Real holds (bD ((sin (#) sin),h)) . x = (1 / 2) * ((cos (2 * (x - h))) - (cos (2 * x)))
proof
let h, x be Real; ::_thesis: (bD ((sin (#) sin),h)) . x = (1 / 2) * ((cos (2 * (x - h))) - (cos (2 * x)))
(bD ((sin (#) sin),h)) . x = ((sin (#) sin) . x) - ((sin (#) sin) . (x - h)) by DIFF_1:4
.= ((sin . x) * (sin . x)) - ((sin (#) sin) . (x - h)) by VALUED_1:5
.= ((sin x) * (sin x)) - ((sin (x - h)) * (sin (x - h))) by VALUED_1:5
.= (- ((1 / 2) * ((cos (x + x)) - (cos (x - x))))) - ((sin (x - h)) * (sin (x - h))) by SIN_COS4:29
.= (- ((1 / 2) * ((cos (2 * x)) - (cos 0)))) - (- ((1 / 2) * ((cos ((x - h) + (x - h))) - (cos ((x - h) - (x - h)))))) by SIN_COS4:29 ;
hence  (bD ((sin (#) sin),h)) . x = (1 / 2) * ((cos (2 * (x - h))) - (cos (2 * x))) ; ::_thesis: verum
end;

theorem :: DIFF_2:52
for h, x being Real holds (cD ((sin (#) sin),h)) . x = (1 / 2) * ((cos ((2 * x) - h)) - (cos ((2 * x) + h)))
proof
let h, x be Real; ::_thesis: (cD ((sin (#) sin),h)) . x = (1 / 2) * ((cos ((2 * x) - h)) - (cos ((2 * x) + h)))
(cD ((sin (#) sin),h)) . x = ((sin (#) sin) . (x + (h / 2))) - ((sin (#) sin) . (x - (h / 2))) by DIFF_1:5
.= ((sin . (x + (h / 2))) * (sin . (x + (h / 2)))) - ((sin (#) sin) . (x - (h / 2))) by VALUED_1:5
.= ((sin (x + (h / 2))) * (sin (x + (h / 2)))) - ((sin (x - (h / 2))) * (sin (x - (h / 2)))) by VALUED_1:5
.= (- ((1 / 2) * ((cos ((x + (h / 2)) + (x + (h / 2)))) - (cos ((x + (h / 2)) - (x + (h / 2))))))) - ((sin (x - (h / 2))) * (sin (x - (h / 2)))) by SIN_COS4:29
.= (- ((1 / 2) * ((cos (2 * (x + (h / 2)))) - (cos 0)))) - (- ((1 / 2) * ((cos ((x - (h / 2)) + (x - (h / 2)))) - (cos ((x - (h / 2)) - (x - (h / 2))))))) by SIN_COS4:29 ;
hence  (cD ((sin (#) sin),h)) . x = (1 / 2) * ((cos ((2 * x) - h)) - (cos ((2 * x) + h))) ; ::_thesis: verum
end;

theorem :: DIFF_2:53
for x0, x1 being Real holds [!(sin (#) cos),x0,x1!] = ((1 / 2) * ((sin (2 * x0)) - (sin (2 * x1)))) / (x0 - x1)
proof
let x0, x1 be Real; ::_thesis: [!(sin (#) cos),x0,x1!] = ((1 / 2) * ((sin (2 * x0)) - (sin (2 * x1)))) / (x0 - x1)
[!(sin (#) cos),x0,x1!] = (((sin . x0) * (cos . x0)) - ((sin (#) cos) . x1)) / (x0 - x1) by VALUED_1:5
.= (((sin x0) * (cos x0)) - ((sin x1) * (cos x1))) / (x0 - x1) by VALUED_1:5
.= (((1 / 2) * ((sin (x0 + x0)) + (sin (x0 - x0)))) - ((sin x1) * (cos x1))) / (x0 - x1) by SIN_COS4:30
.= (((1 / 2) * ((sin (x0 + x0)) + (sin (x0 - x0)))) - ((1 / 2) * ((sin (x1 + x1)) + (sin (x1 - x1))))) / (x0 - x1) by SIN_COS4:30
.= ((1 / 2) * ((sin (2 * x0)) - (sin (2 * x1)))) / (x0 - x1) ;
hence  [!(sin (#) cos),x0,x1!] = ((1 / 2) * ((sin (2 * x0)) - (sin (2 * x1)))) / (x0 - x1) ; ::_thesis: verum
end;

theorem :: DIFF_2:54
for h, x being Real holds (fD ((sin (#) cos),h)) . x = (1 / 2) * ((sin (2 * (x + h))) - (sin (2 * x)))
proof
let h, x be Real; ::_thesis: (fD ((sin (#) cos),h)) . x = (1 / 2) * ((sin (2 * (x + h))) - (sin (2 * x)))
(fD ((sin (#) cos),h)) . x = ((sin (#) cos) . (x + h)) - ((sin (#) cos) . x) by DIFF_1:3
.= ((sin . (x + h)) * (cos . (x + h))) - ((sin (#) cos) . x) by VALUED_1:5
.= ((sin (x + h)) * (cos (x + h))) - ((sin x) * (cos x)) by VALUED_1:5
.= ((1 / 2) * ((sin ((x + h) + (x + h))) + (sin ((x + h) - (x + h))))) - ((sin x) * (cos x)) by SIN_COS4:30
.= ((1 / 2) * ((sin (2 * (x + h))) + (sin 0))) - ((1 / 2) * ((sin (x + x)) + (sin (x - x)))) by SIN_COS4:30
.= ((1 / 2) * (sin (2 * (x + h)))) - ((1 / 2) * (sin (2 * x))) ;
hence  (fD ((sin (#) cos),h)) . x = (1 / 2) * ((sin (2 * (x + h))) - (sin (2 * x))) ; ::_thesis: verum
end;

theorem :: DIFF_2:55
for h, x being Real holds (bD ((sin (#) cos),h)) . x = (1 / 2) * ((sin (2 * x)) - (sin (2 * (x - h))))
proof
let h, x be Real; ::_thesis: (bD ((sin (#) cos),h)) . x = (1 / 2) * ((sin (2 * x)) - (sin (2 * (x - h))))
(bD ((sin (#) cos),h)) . x = ((sin (#) cos) . x) - ((sin (#) cos) . (x - h)) by DIFF_1:4
.= ((sin . x) * (cos . x)) - ((sin (#) cos) . (x - h)) by VALUED_1:5
.= ((sin x) * (cos x)) - ((sin (x - h)) * (cos (x - h))) by VALUED_1:5
.= ((1 / 2) * ((sin (x + x)) + (sin (x - x)))) - ((sin (x - h)) * (cos (x - h))) by SIN_COS4:30
.= ((1 / 2) * ((sin (x + x)) + (sin 0))) - ((1 / 2) * ((sin ((x - h) + (x - h))) + (sin ((x - h) - (x - h))))) by SIN_COS4:30
.= ((1 / 2) * (sin (2 * x))) - ((1 / 2) * (sin (2 * (x - h)))) ;
hence  (bD ((sin (#) cos),h)) . x = (1 / 2) * ((sin (2 * x)) - (sin (2 * (x - h)))) ; ::_thesis: verum
end;

theorem :: DIFF_2:56
for h, x being Real holds (cD ((sin (#) cos),h)) . x = (1 / 2) * ((sin ((2 * x) + h)) - (sin ((2 * x) - h)))
proof
let h, x be Real; ::_thesis: (cD ((sin (#) cos),h)) . x = (1 / 2) * ((sin ((2 * x) + h)) - (sin ((2 * x) - h)))
(cD ((sin (#) cos),h)) . x = ((sin (#) cos) . (x + (h / 2))) - ((sin (#) cos) . (x - (h / 2))) by DIFF_1:5
.= ((sin . (x + (h / 2))) * (cos . (x + (h / 2)))) - ((sin (#) cos) . (x - (h / 2))) by VALUED_1:5
.= ((sin (x + (h / 2))) * (cos (x + (h / 2)))) - ((sin (x - (h / 2))) * (cos (x - (h / 2)))) by VALUED_1:5
.= ((1 / 2) * ((sin ((x + (h / 2)) + (x + (h / 2)))) + (sin ((x + (h / 2)) - (x + (h / 2)))))) - ((sin (x - (h / 2))) * (cos (x - (h / 2)))) by SIN_COS4:30
.= ((1 / 2) * ((sin ((x + (h / 2)) + (x + (h / 2)))) + (sin ((x + (h / 2)) - (x + (h / 2)))))) - ((1 / 2) * ((sin ((x - (h / 2)) + (x - (h / 2)))) + (sin ((x - (h / 2)) - (x - (h / 2)))))) by SIN_COS4:30
.= ((1 / 2) * (sin (2 * (x + (h / 2))))) - ((1 / 2) * (sin (2 * (x - (h / 2))))) ;
hence  (cD ((sin (#) cos),h)) . x = (1 / 2) * ((sin ((2 * x) + h)) - (sin ((2 * x) - h))) ; ::_thesis: verum
end;

theorem :: DIFF_2:57
for x0, x1 being Real holds [!(cos (#) cos),x0,x1!] = ((1 / 2) * ((cos (2 * x0)) - (cos (2 * x1)))) / (x0 - x1)
proof
let x0, x1 be Real; ::_thesis: [!(cos (#) cos),x0,x1!] = ((1 / 2) * ((cos (2 * x0)) - (cos (2 * x1)))) / (x0 - x1)
[!(cos (#) cos),x0,x1!] = (((cos . x0) * (cos . x0)) - ((cos (#) cos) . x1)) / (x0 - x1) by VALUED_1:5
.= (((cos x0) * (cos x0)) - ((cos x1) * (cos x1))) / (x0 - x1) by VALUED_1:5
.= (((1 / 2) * ((cos (x0 + x0)) + (cos (x0 - x0)))) - ((cos x1) * (cos x1))) / (x0 - x1) by SIN_COS4:32
.= (((1 / 2) * ((cos (x0 + x0)) + (cos (x0 - x0)))) - ((1 / 2) * ((cos (x1 + x1)) + (cos (x1 - x1))))) / (x0 - x1) by SIN_COS4:32
.= (((1 / 2) * (cos (2 * x0))) - ((1 / 2) * (cos (2 * x1)))) / (x0 - x1) ;
hence  [!(cos (#) cos),x0,x1!] = ((1 / 2) * ((cos (2 * x0)) - (cos (2 * x1)))) / (x0 - x1) ; ::_thesis: verum
end;

theorem :: DIFF_2:58
for h, x being Real holds (fD ((cos (#) cos),h)) . x = (1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))
proof
let h, x be Real; ::_thesis: (fD ((cos (#) cos),h)) . x = (1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))
(fD ((cos (#) cos),h)) . x = ((cos (#) cos) . (x + h)) - ((cos (#) cos) . x) by DIFF_1:3
.= ((cos . (x + h)) * (cos . (x + h))) - ((cos (#) cos) . x) by VALUED_1:5
.= ((cos (x + h)) * (cos (x + h))) - ((cos x) * (cos x)) by VALUED_1:5
.= ((1 / 2) * ((cos ((x + h) + (x + h))) + (cos ((x + h) - (x + h))))) - ((cos x) * (cos x)) by SIN_COS4:32
.= ((1 / 2) * ((cos (2 * (x + h))) + (cos 0))) - ((1 / 2) * ((cos (x + x)) + (cos (x - x)))) by SIN_COS4:32
.= ((1 / 2) * (cos (2 * (x + h)))) - ((1 / 2) * (cos (2 * x))) ;
hence  (fD ((cos (#) cos),h)) . x = (1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x))) ; ::_thesis: verum
end;

theorem :: DIFF_2:59
for h, x being Real holds (bD ((cos (#) cos),h)) . x = (1 / 2) * ((cos (2 * x)) - (cos (2 * (x - h))))
proof
let h, x be Real; ::_thesis: (bD ((cos (#) cos),h)) . x = (1 / 2) * ((cos (2 * x)) - (cos (2 * (x - h))))
(bD ((cos (#) cos),h)) . x = ((cos (#) cos) . x) - ((cos (#) cos) . (x - h)) by DIFF_1:4
.= ((cos . x) * (cos . x)) - ((cos (#) cos) . (x - h)) by VALUED_1:5
.= ((cos x) * (cos x)) - ((cos (x - h)) * (cos (x - h))) by VALUED_1:5
.= ((1 / 2) * ((cos (x + x)) + (cos (x - x)))) - ((cos (x - h)) * (cos (x - h))) by SIN_COS4:32
.= ((1 / 2) * ((cos (x + x)) + (cos (x - x)))) - ((1 / 2) * ((cos ((x - h) + (x - h))) + (cos ((x - h) - (x - h))))) by SIN_COS4:32
.= ((1 / 2) * (cos (2 * x))) - ((1 / 2) * (cos (2 * (x - h)))) ;
hence  (bD ((cos (#) cos),h)) . x = (1 / 2) * ((cos (2 * x)) - (cos (2 * (x - h)))) ; ::_thesis: verum
end;

theorem :: DIFF_2:60
for h, x being Real holds (cD ((cos (#) cos),h)) . x = (1 / 2) * ((cos ((2 * x) + h)) - (cos ((2 * x) - h)))
proof
let h, x be Real; ::_thesis: (cD ((cos (#) cos),h)) . x = (1 / 2) * ((cos ((2 * x) + h)) - (cos ((2 * x) - h)))
(cD ((cos (#) cos),h)) . x = ((cos (#) cos) . (x + (h / 2))) - ((cos (#) cos) . (x - (h / 2))) by DIFF_1:5
.= ((cos . (x + (h / 2))) * (cos . (x + (h / 2)))) - ((cos (#) cos) . (x - (h / 2))) by VALUED_1:5
.= ((cos (x + (h / 2))) * (cos (x + (h / 2)))) - ((cos (x - (h / 2))) * (cos (x - (h / 2)))) by VALUED_1:5
.= ((1 / 2) * ((cos ((x + (h / 2)) + (x + (h / 2)))) + (cos ((x + (h / 2)) - (x + (h / 2)))))) - ((cos (x - (h / 2))) * (cos (x - (h / 2)))) by SIN_COS4:32
.= ((1 / 2) * ((cos ((x + (h / 2)) + (x + (h / 2)))) + (cos ((x + (h / 2)) - (x + (h / 2)))))) - ((1 / 2) * ((cos ((x - (h / 2)) + (x - (h / 2)))) + (cos ((x - (h / 2)) - (x - (h / 2)))))) by SIN_COS4:32
.= ((1 / 2) * (cos (2 * (x + (h / 2))))) - ((1 / 2) * (cos (2 * (x - (h / 2))))) ;
hence  (cD ((cos (#) cos),h)) . x = (1 / 2) * ((cos ((2 * x) + h)) - (cos ((2 * x) - h))) ; ::_thesis: verum
end;

theorem :: DIFF_2:61
for x0, x1 being Real holds [!((sin (#) sin) (#) cos),x0,x1!] = - (((1 / 2) * (((sin ((3 * (x1 + x0)) / 2)) * (sin ((3 * (x1 - x0)) / 2))) + ((sin ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2))))) / (x0 - x1))
proof
let x0, x1 be Real; ::_thesis: [!((sin (#) sin) (#) cos),x0,x1!] = - (((1 / 2) * (((sin ((3 * (x1 + x0)) / 2)) * (sin ((3 * (x1 - x0)) / 2))) + ((sin ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2))))) / (x0 - x1))
set y = 3 * x0;
set z = 3 * x1;
[!((sin (#) sin) (#) cos),x0,x1!] = ((((sin (#) sin) . x0) * (cos . x0)) - (((sin (#) sin) (#) cos) . x1)) / (x0 - x1) by VALUED_1:5
.= ((((sin . x0) * (sin . x0)) * (cos . x0)) - (((sin (#) sin) (#) cos) . x1)) / (x0 - x1) by VALUED_1:5
.= ((((sin . x0) * (sin . x0)) * (cos . x0)) - (((sin (#) sin) . x1) * (cos . x1))) / (x0 - x1) by VALUED_1:5
.= ((((sin x0) * (sin x0)) * (cos x0)) - (((sin x1) * (sin x1)) * (cos x1))) / (x0 - x1) by VALUED_1:5
.= (((1 / 4) * ((((- (cos ((x0 + x0) - x0))) + (cos ((x0 + x0) - x0))) + (cos ((x0 + x0) - x0))) - (cos ((x0 + x0) + x0)))) - (((sin x1) * (sin x1)) * (cos x1))) / (x0 - x1) by SIN_COS4:34
.= (((1 / 4) * ((cos x0) - (cos (3 * x0)))) - ((1 / 4) * ((((- (cos ((x1 + x1) - x1))) + (cos ((x1 + x1) - x1))) + (cos ((x1 + x1) - x1))) - (cos ((x1 + x1) + x1))))) / (x0 - x1) by SIN_COS4:34
.= (((1 / 4) * ((cos x0) - (cos x1))) + ((1 / 4) * ((cos (3 * x1)) - (cos (3 * x0))))) / (x0 - x1)
.= (((1 / 4) * (- (2 * ((sin ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2)))))) + ((1 / 4) * ((cos (3 * x1)) - (cos (3 * x0))))) / (x0 - x1) by SIN_COS4:18
.= (((1 / 4) * (- (2 * ((sin ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2)))))) + ((1 / 4) * (- (2 * ((sin (((3 * x1) + (3 * x0)) / 2)) * (sin (((3 * x1) - (3 * x0)) / 2))))))) / (x0 - x1) by SIN_COS4:18
.= (- ((1 / 2) * (((sin ((3 * (x1 + x0)) / 2)) * (sin ((3 * (x1 - x0)) / 2))) + ((sin ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2)))))) / (x0 - x1) ;
hence  [!((sin (#) sin) (#) cos),x0,x1!] = - (((1 / 2) * (((sin ((3 * (x1 + x0)) / 2)) * (sin ((3 * (x1 - x0)) / 2))) + ((sin ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2))))) / (x0 - x1)) by XCMPLX_1:187; ::_thesis: verum
end;

theorem :: DIFF_2:62
for h, x being Real holds (fD (((sin (#) sin) (#) cos),h)) . x = (1 / 2) * (((sin (((6 * x) + (3 * h)) / 2)) * (sin ((3 * h) / 2))) - ((sin (((2 * x) + h) / 2)) * (sin (h / 2))))
proof
let h, x be Real; ::_thesis: (fD (((sin (#) sin) (#) cos),h)) . x = (1 / 2) * (((sin (((6 * x) + (3 * h)) / 2)) * (sin ((3 * h) / 2))) - ((sin (((2 * x) + h) / 2)) * (sin (h / 2))))
set y = 3 * x;
set z = 3 * h;
(fD (((sin (#) sin) (#) cos),h)) . x = (((sin (#) sin) (#) cos) . (x + h)) - (((sin (#) sin) (#) cos) . x) by DIFF_1:3
.= (((sin (#) sin) . (x + h)) * (cos . (x + h))) - (((sin (#) sin) (#) cos) . x) by VALUED_1:5
.= (((sin . (x + h)) * (sin . (x + h))) * (cos . (x + h))) - (((sin (#) sin) (#) cos) . x) by VALUED_1:5
.= (((sin . (x + h)) * (sin . (x + h))) * (cos . (x + h))) - (((sin (#) sin) . x) * (cos . x)) by VALUED_1:5
.= (((sin (x + h)) * (sin (x + h))) * (cos (x + h))) - (((sin x) * (sin x)) * (cos x)) by VALUED_1:5
.= ((1 / 4) * ((((- (cos (((x + h) + (x + h)) - (x + h)))) + (cos (((x + h) + (x + h)) - (x + h)))) + (cos (((x + h) + (x + h)) - (x + h)))) - (cos (((x + h) + (x + h)) + (x + h))))) - (((sin x) * (sin x)) * (cos x)) by SIN_COS4:34
.= ((1 / 4) * ((cos (x + h)) - (cos (3 * (x + h))))) - ((1 / 4) * ((((- (cos ((x + x) - x))) + (cos ((x + x) - x))) + (cos ((x + x) - x))) - (cos ((x + x) + x)))) by SIN_COS4:34
.= ((1 / 4) * ((cos (x + h)) - (cos x))) - ((1 / 4) * ((cos (3 * (x + h))) - (cos (3 * x))))
.= ((1 / 4) * (- (2 * ((sin (((x + h) + x) / 2)) * (sin (((x + h) - x) / 2)))))) - ((1 / 4) * ((cos (3 * (x + h))) - (cos (3 * x)))) by SIN_COS4:18
.= ((1 / 4) * (- (2 * ((sin (((2 * x) + h) / 2)) * (sin (h / 2)))))) - ((1 / 4) * (- (2 * ((sin ((((3 * x) + (3 * h)) + (3 * x)) / 2)) * (sin ((((3 * x) + (3 * h)) - (3 * x)) / 2)))))) by SIN_COS4:18
.= ((1 / 2) * ((sin (((6 * x) + (3 * h)) / 2)) * (sin ((3 * h) / 2)))) - ((1 / 2) * ((sin (((2 * x) + h) / 2)) * (sin (h / 2)))) ;
hence  (fD (((sin (#) sin) (#) cos),h)) . x = (1 / 2) * (((sin (((6 * x) + (3 * h)) / 2)) * (sin ((3 * h) / 2))) - ((sin (((2 * x) + h) / 2)) * (sin (h / 2)))) ; ::_thesis: verum
end;

theorem :: DIFF_2:63
for h, x being Real holds (bD (((sin (#) sin) (#) cos),h)) . x = ((1 / 2) * ((sin (((6 * x) - (3 * h)) / 2)) * (sin ((3 * h) / 2)))) - ((1 / 2) * ((sin (((2 * x) - h) / 2)) * (sin (h / 2))))
proof
let h, x be Real; ::_thesis: (bD (((sin (#) sin) (#) cos),h)) . x = ((1 / 2) * ((sin (((6 * x) - (3 * h)) / 2)) * (sin ((3 * h) / 2)))) - ((1 / 2) * ((sin (((2 * x) - h) / 2)) * (sin (h / 2))))
set y = 3 * x;
set z = 3 * h;
(bD (((sin (#) sin) (#) cos),h)) . x = (((sin (#) sin) (#) cos) . x) - (((sin (#) sin) (#) cos) . (x - h)) by DIFF_1:4
.= (((sin (#) sin) . x) * (cos . x)) - (((sin (#) sin) (#) cos) . (x - h)) by VALUED_1:5
.= (((sin . x) * (sin . x)) * (cos . x)) - (((sin (#) sin) (#) cos) . (x - h)) by VALUED_1:5
.= (((sin . x) * (sin . x)) * (cos . x)) - (((sin (#) sin) . (x - h)) * (cos . (x - h))) by VALUED_1:5
.= (((sin x) * (sin x)) * (cos x)) - (((sin (x - h)) * (sin (x - h))) * (cos (x - h))) by VALUED_1:5
.= ((1 / 4) * ((((- (cos ((x + x) - x))) + (cos ((x + x) - x))) + (cos ((x + x) - x))) - (cos ((x + x) + x)))) - (((sin (x - h)) * (sin (x - h))) * (cos (x - h))) by SIN_COS4:34
.= ((1 / 4) * ((cos x) - (cos (3 * x)))) - ((1 / 4) * ((((- (cos (((x - h) + (x - h)) - (x - h)))) + (cos (((x - h) + (x - h)) - (x - h)))) + (cos (((x - h) + (x - h)) - (x - h)))) - (cos (((x - h) + (x - h)) + (x - h))))) by SIN_COS4:34
.= ((1 / 4) * ((cos x) - (cos (x - h)))) - ((1 / 4) * ((cos (3 * x)) - (cos (3 * (x - h)))))
.= ((1 / 4) * (- (2 * ((sin ((x + (x - h)) / 2)) * (sin ((x - (x - h)) / 2)))))) - ((1 / 4) * ((cos (3 * x)) - (cos (3 * (x - h))))) by SIN_COS4:18
.= ((1 / 4) * (- (2 * ((sin (((2 * x) - h) / 2)) * (sin (h / 2)))))) - ((1 / 4) * (- (2 * ((sin (((3 * x) + ((3 * x) - (3 * h))) / 2)) * (sin (((3 * x) - ((3 * x) - (3 * h))) / 2)))))) by SIN_COS4:18
.= ((1 / 2) * ((sin (((6 * x) - (3 * h)) / 2)) * (sin ((3 * h) / 2)))) - ((1 / 2) * ((sin (((2 * x) - h) / 2)) * (sin (h / 2)))) ;
hence  (bD (((sin (#) sin) (#) cos),h)) . x = ((1 / 2) * ((sin (((6 * x) - (3 * h)) / 2)) * (sin ((3 * h) / 2)))) - ((1 / 2) * ((sin (((2 * x) - h) / 2)) * (sin (h / 2)))) ; ::_thesis: verum
end;

theorem :: DIFF_2:64
for h, x being Real holds (cD (((sin (#) sin) (#) cos),h)) . x = (- ((1 / 2) * ((sin x) * (sin (h / 2))))) + ((1 / 2) * ((sin (3 * x)) * (sin ((3 * h) / 2))))
proof
let h, x be Real; ::_thesis: (cD (((sin (#) sin) (#) cos),h)) . x = (- ((1 / 2) * ((sin x) * (sin (h / 2))))) + ((1 / 2) * ((sin (3 * x)) * (sin ((3 * h) / 2))))
set y = 3 * x;
set z = 3 * h;
(cD (((sin (#) sin) (#) cos),h)) . x = (((sin (#) sin) (#) cos) . (x + (h / 2))) - (((sin (#) sin) (#) cos) . (x - (h / 2))) by DIFF_1:5
.= (((sin (#) sin) . (x + (h / 2))) * (cos . (x + (h / 2)))) - (((sin (#) sin) (#) cos) . (x - (h / 2))) by VALUED_1:5
.= (((sin . (x + (h / 2))) * (sin . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((sin (#) sin) (#) cos) . (x - (h / 2))) by VALUED_1:5
.= (((sin . (x + (h / 2))) * (sin . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((sin (#) sin) . (x - (h / 2))) * (cos . (x - (h / 2)))) by VALUED_1:5
.= (((sin (x + (h / 2))) * (sin (x + (h / 2)))) * (cos (x + (h / 2)))) - (((sin (x - (h / 2))) * (sin (x - (h / 2)))) * (cos (x - (h / 2)))) by VALUED_1:5
.= ((1 / 4) * ((((- (cos (((x + (h / 2)) + (x + (h / 2))) - (x + (h / 2))))) + (cos (((x + (h / 2)) + (x + (h / 2))) - (x + (h / 2))))) + (cos (((x + (h / 2)) + (x + (h / 2))) - (x + (h / 2))))) - (cos (((x + (h / 2)) + (x + (h / 2))) + (x + (h / 2)))))) - (((sin (x - (h / 2))) * (sin (x - (h / 2)))) * (cos (x - (h / 2)))) by SIN_COS4:34
.= ((1 / 4) * ((cos (x + (h / 2))) - (cos (3 * (x + (h / 2)))))) - ((1 / 4) * ((((- (cos (((x - (h / 2)) + (x - (h / 2))) - (x - (h / 2))))) + (cos (((x - (h / 2)) + (x - (h / 2))) - (x - (h / 2))))) + (cos (((x - (h / 2)) + (x - (h / 2))) - (x - (h / 2))))) - (cos (((x - (h / 2)) + (x - (h / 2))) + (x - (h / 2)))))) by SIN_COS4:34
.= ((1 / 4) * ((cos (x + (h / 2))) - (cos (x - (h / 2))))) - ((1 / 4) * ((cos (3 * (x + (h / 2)))) - (cos (3 * (x - (h / 2))))))
.= ((1 / 4) * (- (2 * ((sin (((x + (h / 2)) + (x - (h / 2))) / 2)) * (sin (((x + (h / 2)) - (x - (h / 2))) / 2)))))) - ((1 / 4) * ((cos (3 * (x + (h / 2)))) - (cos (3 * (x - (h / 2)))))) by SIN_COS4:18
.= ((1 / 4) * (- (2 * ((sin x) * (sin (h / 2)))))) - ((1 / 4) * (- (2 * ((sin ((((3 * x) + ((3 * h) / 2)) + ((3 * x) - ((3 * h) / 2))) / 2)) * (sin ((((3 * x) + ((3 * h) / 2)) - ((3 * x) - ((3 * h) / 2))) / 2)))))) by SIN_COS4:18
.= (- ((1 / 2) * ((sin x) * (sin (h / 2))))) + ((1 / 2) * ((sin (3 * x)) * (sin ((3 * h) / 2)))) ;
hence  (cD (((sin (#) sin) (#) cos),h)) . x = (- ((1 / 2) * ((sin x) * (sin (h / 2))))) + ((1 / 2) * ((sin (3 * x)) * (sin ((3 * h) / 2)))) ; ::_thesis: verum
end;

theorem :: DIFF_2:65
for x0, x1 being Real holds [!((sin (#) cos) (#) cos),x0,x1!] = ((1 / 2) * (((cos ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2))) + ((cos ((3 * (x0 + x1)) / 2)) * (sin ((3 * (x0 - x1)) / 2))))) / (x0 - x1)
proof
let x0, x1 be Real; ::_thesis: [!((sin (#) cos) (#) cos),x0,x1!] = ((1 / 2) * (((cos ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2))) + ((cos ((3 * (x0 + x1)) / 2)) * (sin ((3 * (x0 - x1)) / 2))))) / (x0 - x1)
set y = 3 * x0;
set z = 3 * x1;
[!((sin (#) cos) (#) cos),x0,x1!] = ((((sin (#) cos) . x0) * (cos . x0)) - (((sin (#) cos) (#) cos) . x1)) / (x0 - x1) by VALUED_1:5
.= ((((sin . x0) * (cos . x0)) * (cos . x0)) - (((sin (#) cos) (#) cos) . x1)) / (x0 - x1) by VALUED_1:5
.= ((((sin . x0) * (cos . x0)) * (cos . x0)) - (((sin (#) cos) . x1) * (cos . x1))) / (x0 - x1) by VALUED_1:5
.= ((((sin x0) * (cos x0)) * (cos x0)) - (((sin x1) * (cos x1)) * (cos x1))) / (x0 - x1) by VALUED_1:5
.= (((1 / 4) * ((((sin ((x0 + x0) - x0)) - (sin ((x0 + x0) - x0))) + (sin ((x0 + x0) - x0))) + (sin ((x0 + x0) + x0)))) - (((sin x1) * (cos x1)) * (cos x1))) / (x0 - x1) by SIN_COS4:35
.= (((1 / 4) * ((sin x0) + (sin (3 * x0)))) - ((1 / 4) * ((((sin ((x1 + x1) - x1)) - (sin ((x1 + x1) - x1))) + (sin ((x1 + x1) - x1))) + (sin ((x1 + x1) + x1))))) / (x0 - x1) by SIN_COS4:35
.= (((1 / 4) * ((sin x0) - (sin x1))) + ((1 / 4) * ((sin (3 * x0)) - (sin (3 * x1))))) / (x0 - x1)
.= (((1 / 4) * (2 * ((cos ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2))))) + ((1 / 4) * ((sin (3 * x0)) - (sin (3 * x1))))) / (x0 - x1) by SIN_COS4:16
.= (((1 / 2) * ((cos ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2)))) + ((1 / 4) * (2 * ((cos (((3 * x0) + (3 * x1)) / 2)) * (sin (((3 * x0) - (3 * x1)) / 2)))))) / (x0 - x1) by SIN_COS4:16
.= ((1 / 2) * (((cos ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2))) + ((cos ((3 * (x0 + x1)) / 2)) * (sin ((3 * (x0 - x1)) / 2))))) / (x0 - x1) ;
hence  [!((sin (#) cos) (#) cos),x0,x1!] = ((1 / 2) * (((cos ((x0 + x1) / 2)) * (sin ((x0 - x1) / 2))) + ((cos ((3 * (x0 + x1)) / 2)) * (sin ((3 * (x0 - x1)) / 2))))) / (x0 - x1) ; ::_thesis: verum
end;

theorem :: DIFF_2:66
for h, x being Real holds (fD (((sin (#) cos) (#) cos),h)) . x = (1 / 2) * (((cos (((2 * x) + h) / 2)) * (sin (h / 2))) + ((cos (((6 * x) + (3 * h)) / 2)) * (sin ((3 * h) / 2))))
proof
let h, x be Real; ::_thesis: (fD (((sin (#) cos) (#) cos),h)) . x = (1 / 2) * (((cos (((2 * x) + h) / 2)) * (sin (h / 2))) + ((cos (((6 * x) + (3 * h)) / 2)) * (sin ((3 * h) / 2))))
set y = 3 * x;
set z = 3 * h;
(fD (((sin (#) cos) (#) cos),h)) . x = (((sin (#) cos) (#) cos) . (x + h)) - (((sin (#) cos) (#) cos) . x) by DIFF_1:3
.= (((sin (#) cos) . (x + h)) * (cos . (x + h))) - (((sin (#) cos) (#) cos) . x) by VALUED_1:5
.= (((sin . (x + h)) * (cos . (x + h))) * (cos . (x + h))) - (((sin (#) cos) (#) cos) . x) by VALUED_1:5
.= (((sin . (x + h)) * (cos . (x + h))) * (cos . (x + h))) - (((sin (#) cos) . x) * (cos . x)) by VALUED_1:5
.= (((sin (x + h)) * (cos (x + h))) * (cos (x + h))) - (((sin x) * (cos x)) * (cos x)) by VALUED_1:5
.= ((1 / 4) * ((((sin (((x + h) + (x + h)) - (x + h))) - (sin (((x + h) + (x + h)) - (x + h)))) + (sin (((x + h) + (x + h)) - (x + h)))) + (sin (((x + h) + (x + h)) + (x + h))))) - (((sin x) * (cos x)) * (cos x)) by SIN_COS4:35
.= ((1 / 4) * ((sin (x + h)) + (sin (3 * (x + h))))) - ((1 / 4) * ((((sin ((x + x) - x)) - (sin ((x + x) - x))) + (sin ((x + x) - x))) + (sin ((x + x) + x)))) by SIN_COS4:35
.= ((1 / 4) * ((sin (x + h)) - (sin x))) + ((1 / 4) * ((sin (3 * (x + h))) - (sin (3 * x))))
.= ((1 / 4) * (2 * ((cos (((x + h) + x) / 2)) * (sin (((x + h) - x) / 2))))) + ((1 / 4) * ((sin (3 * (x + h))) - (sin (3 * x)))) by SIN_COS4:16
.= ((1 / 4) * (2 * ((cos (((2 * x) + h) / 2)) * (sin (h / 2))))) + ((1 / 4) * (2 * ((cos ((((3 * x) + (3 * h)) + (3 * x)) / 2)) * (sin ((((3 * x) + (3 * h)) - (3 * x)) / 2))))) by SIN_COS4:16
.= ((1 / 2) * ((cos (((2 * x) + h) / 2)) * (sin (h / 2)))) + ((1 / 2) * ((cos (((6 * x) + (3 * h)) / 2)) * (sin ((3 * h) / 2)))) ;
hence  (fD (((sin (#) cos) (#) cos),h)) . x = (1 / 2) * (((cos (((2 * x) + h) / 2)) * (sin (h / 2))) + ((cos (((6 * x) + (3 * h)) / 2)) * (sin ((3 * h) / 2)))) ; ::_thesis: verum
end;

theorem :: DIFF_2:67
for h, x being Real holds (bD (((sin (#) cos) (#) cos),h)) . x = (1 / 2) * (((cos (((2 * x) - h) / 2)) * (sin (h / 2))) + ((cos (((6 * x) - (3 * h)) / 2)) * (sin ((3 * h) / 2))))
proof
let h, x be Real; ::_thesis: (bD (((sin (#) cos) (#) cos),h)) . x = (1 / 2) * (((cos (((2 * x) - h) / 2)) * (sin (h / 2))) + ((cos (((6 * x) - (3 * h)) / 2)) * (sin ((3 * h) / 2))))
set y = 3 * x;
set z = 3 * h;
(bD (((sin (#) cos) (#) cos),h)) . x = (((sin (#) cos) (#) cos) . x) - (((sin (#) cos) (#) cos) . (x - h)) by DIFF_1:4
.= (((sin (#) cos) . x) * (cos . x)) - (((sin (#) cos) (#) cos) . (x - h)) by VALUED_1:5
.= (((sin . x) * (cos . x)) * (cos . x)) - (((sin (#) cos) (#) cos) . (x - h)) by VALUED_1:5
.= (((sin . x) * (cos . x)) * (cos . x)) - (((sin (#) cos) . (x - h)) * (cos . (x - h))) by VALUED_1:5
.= (((sin x) * (cos x)) * (cos x)) - (((sin (x - h)) * (cos (x - h))) * (cos (x - h))) by VALUED_1:5
.= ((1 / 4) * ((((sin ((x + x) - x)) - (sin ((x + x) - x))) + (sin ((x + x) - x))) + (sin ((x + x) + x)))) - (((sin (x - h)) * (cos (x - h))) * (cos (x - h))) by SIN_COS4:35
.= ((1 / 4) * ((sin x) + (sin (3 * x)))) - ((1 / 4) * ((((sin (((x - h) + (x - h)) - (x - h))) - (sin (((x - h) + (x - h)) - (x - h)))) + (sin (((x - h) + (x - h)) - (x - h)))) + (sin (((x - h) + (x - h)) + (x - h))))) by SIN_COS4:35
.= ((1 / 4) * ((sin x) - (sin (x - h)))) + ((1 / 4) * ((sin (3 * x)) - (sin (3 * (x - h)))))
.= ((1 / 4) * (2 * ((cos ((x + (x - h)) / 2)) * (sin ((x - (x - h)) / 2))))) + ((1 / 4) * ((sin (3 * x)) - (sin (3 * (x - h))))) by SIN_COS4:16
.= ((1 / 4) * (2 * ((cos (((2 * x) - h) / 2)) * (sin (h / 2))))) + ((1 / 4) * (2 * ((cos (((3 * x) + ((3 * x) - (3 * h))) / 2)) * (sin (((3 * x) - ((3 * x) - (3 * h))) / 2))))) by SIN_COS4:16
.= ((1 / 2) * ((cos (((2 * x) - h) / 2)) * (sin (h / 2)))) + ((1 / 2) * ((cos (((6 * x) - (3 * h)) / 2)) * (sin ((3 * h) / 2)))) ;
hence  (bD (((sin (#) cos) (#) cos),h)) . x = (1 / 2) * (((cos (((2 * x) - h) / 2)) * (sin (h / 2))) + ((cos (((6 * x) - (3 * h)) / 2)) * (sin ((3 * h) / 2)))) ; ::_thesis: verum
end;

theorem :: DIFF_2:68
for h, x being Real holds (cD (((sin (#) cos) (#) cos),h)) . x = (1 / 2) * (((cos x) * (sin (h / 2))) + ((cos (3 * x)) * (sin ((3 * h) / 2))))
proof
let h, x be Real; ::_thesis: (cD (((sin (#) cos) (#) cos),h)) . x = (1 / 2) * (((cos x) * (sin (h / 2))) + ((cos (3 * x)) * (sin ((3 * h) / 2))))
set y = 3 * x;
set z = 3 * h;
(cD (((sin (#) cos) (#) cos),h)) . x = (((sin (#) cos) (#) cos) . (x + (h / 2))) - (((sin (#) cos) (#) cos) . (x - (h / 2))) by DIFF_1:5
.= (((sin (#) cos) . (x + (h / 2))) * (cos . (x + (h / 2)))) - (((sin (#) cos) (#) cos) . (x - (h / 2))) by VALUED_1:5
.= (((sin . (x + (h / 2))) * (cos . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((sin (#) cos) (#) cos) . (x - (h / 2))) by VALUED_1:5
.= (((sin . (x + (h / 2))) * (cos . (x + (h / 2)))) * (cos . (x + (h / 2)))) - (((sin (#) cos) . (x - (h / 2))) * (cos . (x - (h / 2)))) by VALUED_1:5
.= (((sin (x + (h / 2))) * (cos (x + (h / 2)))) * (cos (x + (h / 2)))) - (((sin (x - (h / 2))) * (cos (x - (h / 2)))) * (cos (x - (h / 2)))) by VALUED_1:5
.= ((1 / 4) * ((((sin (((x + (h / 2)) + (x + (h / 2))) - (x + (h / 2)))) - (sin (((x + (h / 2)) + (x + (h / 2))) - (x + (h / 2))))) + (sin (((x + (h / 2)) + (x + (h / 2))) - (x + (h / 2))))) + (sin (((x + (h / 2)) + (x + (h / 2))) + (x + (h / 2)))))) - (((sin (x - (h / 2))) * (cos (x - (h / 2)))) * (cos (x - (h / 2)))) by SIN_COS4:35
.= ((1 / 4) * ((sin (x + (h / 2))) + (sin (3 * (x + (h / 2)))))) - ((1 / 4) * ((((sin (((x - (h / 2)) + (x - (h / 2))) - (x - (h / 2)))) - (sin (((x - (h / 2)) + (x - (h / 2))) - (x - (h / 2))))) + (sin (((x - (h / 2)) + (x - (h / 2))) - (x - (h / 2))))) + (sin (((x - (h / 2)) + (x - (h / 2))) + (x - (h / 2)))))) by SIN_COS4:35
.= ((1 / 4) * ((sin (x + (h / 2))) - (sin (x - (h / 2))))) + ((1 / 4) * ((sin (3 * (x + (h / 2)))) - (sin (3 * (x - (h / 2))))))
.= ((1 / 4) * (2 * ((cos (((x + (h / 2)) + (x - (h / 2))) / 2)) * (sin (((x + (h / 2)) - (x - (h / 2))) / 2))))) + ((1 / 4) * ((sin (3 * (x + (h / 2)))) - (sin (3 * (x - (h / 2)))))) by SIN_COS4:16
.= ((1 / 4) * (2 * ((cos x) * (sin (h / 2))))) + ((1 / 4) * (2 * ((cos ((((3 * x) + ((3 * h) / 2)) + ((3 * x) - ((3 * h) / 2))) / 2)) * (sin ((((3 * x) + ((3 * h) / 2)) - ((3 * x) - ((3 * h) / 2))) / 2))))) by SIN_COS4:16
.= ((1 / 2) * ((cos x) * (sin (h / 2)))) + ((1 / 2) * ((cos (3 * x)) * (sin ((3 * h) / 2)))) ;
hence  (cD (((sin (#) cos) (#) cos),h)) . x = (1 / 2) * (((cos x) * (sin (h / 2))) + ((cos (3 * x)) * (sin ((3 * h) / 2)))) ; ::_thesis: verum
end;

theorem :: DIFF_2:69
for x0, x1 being Real st x0 in dom tan & x1 in dom tan holds
[!tan,x0,x1!] = (sin (x0 - x1)) / (((cos x0) * (cos x1)) * (x0 - x1))
proof
let x0, x1 be Real; ::_thesis: ( x0 in dom tan & x1 in dom tan implies [!tan,x0,x1!] = (sin (x0 - x1)) / (((cos x0) * (cos x1)) * (x0 - x1)) )
assume that
A1: x0 in dom tan and
A2: x1 in dom tan ; ::_thesis: [!tan,x0,x1!] = (sin (x0 - x1)) / (((cos x0) * (cos x1)) * (x0 - x1))
A3: tan . x0 = (sin . x0) * ((cos . x0) ") by A1, RFUNCT_1:def_1
.= (sin . x0) * (1 / (cos . x0)) by XCMPLX_1:215
.= tan x0 by XCMPLX_1:99 ;
A4: tan . x1 = (sin . x1) * ((cos . x1) ") by A2, RFUNCT_1:def_1
.= (sin . x1) * (1 / (cos . x1)) by XCMPLX_1:215
.= tan x1 by XCMPLX_1:99 ;
 ( cos x0 <> 0 & cos x1 <> 0 ) by A1, A2, FDIFF_8:1;
then [!tan,x0,x1!] = ((sin (x0 - x1)) / ((cos x0) * (cos x1))) / (x0 - x1) by A3, A4, SIN_COS4:20
.= (sin (x0 - x1)) / (((cos x0) * (cos x1)) * (x0 - x1)) by XCMPLX_1:78 ;
hence  [!tan,x0,x1!] = (sin (x0 - x1)) / (((cos x0) * (cos x1)) * (x0 - x1)) ; ::_thesis: verum
end;

theorem :: DIFF_2:70
for x0, x1 being Real st x0 in dom cot & x1 in dom cot holds
[!cot,x0,x1!] = - ((sin (x0 - x1)) / (((sin x0) * (sin x1)) * (x0 - x1)))
proof
let x0, x1 be Real; ::_thesis: ( x0 in dom cot & x1 in dom cot implies [!cot,x0,x1!] = - ((sin (x0 - x1)) / (((sin x0) * (sin x1)) * (x0 - x1))) )
assume that
A1: x0 in dom cot and
A2: x1 in dom cot ; ::_thesis: [!cot,x0,x1!] = - ((sin (x0 - x1)) / (((sin x0) * (sin x1)) * (x0 - x1)))
A3: cot . x0 = (cos . x0) * ((sin . x0) ") by A1, RFUNCT_1:def_1
.= (cos . x0) * (1 / (sin . x0)) by XCMPLX_1:215
.= cot x0 by XCMPLX_1:99 ;
A4: cot . x1 = (cos . x1) * ((sin . x1) ") by A2, RFUNCT_1:def_1
.= (cos . x1) * (1 / (sin . x1)) by XCMPLX_1:215
.= cot x1 by XCMPLX_1:99 ;
 ( sin x0 <> 0 & sin x1 <> 0 ) by A1, A2, FDIFF_8:2;
then [!cot,x0,x1!] = (- ((sin (x0 - x1)) / ((sin x0) * (sin x1)))) / (x0 - x1) by A3, A4, SIN_COS4:24
.= - (((sin (x0 - x1)) / ((sin x0) * (sin x1))) / (x0 - x1)) by XCMPLX_1:187 ;
hence  [!cot,x0,x1!] = - ((sin (x0 - x1)) / (((sin x0) * (sin x1)) * (x0 - x1))) by XCMPLX_1:78; ::_thesis: verum
end;

theorem :: DIFF_2:71
for x0, x1 being Real st x0 in dom cosec & x1 in dom cosec holds
[!cosec,x0,x1!] = ((2 * (cos ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((sin x1) * (sin x0)) * (x0 - x1))
proof
let x0, x1 be Real; ::_thesis: ( x0 in dom cosec & x1 in dom cosec implies [!cosec,x0,x1!] = ((2 * (cos ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((sin x1) * (sin x0)) * (x0 - x1)) )
assume that
A1: x0 in dom cosec and
A2: x1 in dom cosec ; ::_thesis: [!cosec,x0,x1!] = ((2 * (cos ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((sin x1) * (sin x0)) * (x0 - x1))
A3: cosec . x1 = (sin . x1) " by A2, RFUNCT_1:def_2
.= cosec x1 by XCMPLX_1:215 ;
cosec . x0 = (sin . x0) " by A1, RFUNCT_1:def_2
.= cosec x0 by XCMPLX_1:215 ;
then [!cosec,x0,x1!] = (((1 * (sin x1)) / ((sin x0) * (sin x1))) - (1 / (sin x1))) / (x0 - x1) by A2, A3, RFUNCT_1:3, XCMPLX_1:91
.= (((1 * (sin x1)) / ((sin x0) * (sin x1))) - ((1 * (sin x0)) / ((sin x1) * (sin x0)))) / (x0 - x1) by A1, RFUNCT_1:3, XCMPLX_1:91
.= (((sin x1) - (sin x0)) / ((sin x1) * (sin x0))) / (x0 - x1) by XCMPLX_1:120
.= ((sin x1) - (sin x0)) / (((sin x1) * (sin x0)) * (x0 - x1)) by XCMPLX_1:78
.= (2 * ((cos ((x1 + x0) / 2)) * (sin ((x1 - x0) / 2)))) / (((sin x1) * (sin x0)) * (x0 - x1)) by SIN_COS4:16 ;
hence  [!cosec,x0,x1!] = ((2 * (cos ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((sin x1) * (sin x0)) * (x0 - x1)) ; ::_thesis: verum
end;

theorem :: DIFF_2:72
for x0, x1 being Real st x0 in dom sec & x1 in dom sec holds
[!sec,x0,x1!] = - (((2 * (sin ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((cos x1) * (cos x0)) * (x0 - x1)))
proof
let x0, x1 be Real; ::_thesis: ( x0 in dom sec & x1 in dom sec implies [!sec,x0,x1!] = - (((2 * (sin ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((cos x1) * (cos x0)) * (x0 - x1))) )
assume that
A1: x0 in dom sec and
A2: x1 in dom sec ; ::_thesis: [!sec,x0,x1!] = - (((2 * (sin ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((cos x1) * (cos x0)) * (x0 - x1)))
A3: sec . x1 = (cos . x1) " by A2, RFUNCT_1:def_2
.= sec x1 by XCMPLX_1:215 ;
sec . x0 = (cos . x0) " by A1, RFUNCT_1:def_2
.= sec x0 by XCMPLX_1:215 ;
then [!sec,x0,x1!] = (((1 * (cos x1)) / ((cos x0) * (cos x1))) - (1 / (cos x1))) / (x0 - x1) by A2, A3, RFUNCT_1:3, XCMPLX_1:91
.= (((1 * (cos x1)) / ((cos x0) * (cos x1))) - ((1 * (cos x0)) / ((cos x1) * (cos x0)))) / (x0 - x1) by A1, RFUNCT_1:3, XCMPLX_1:91
.= (((cos x1) - (cos x0)) / ((cos x1) * (cos x0))) / (x0 - x1) by XCMPLX_1:120
.= ((cos x1) - (cos x0)) / (((cos x1) * (cos x0)) * (x0 - x1)) by XCMPLX_1:78
.= (- (2 * ((sin ((x1 + x0) / 2)) * (sin ((x1 - x0) / 2))))) / (((cos x1) * (cos x0)) * (x0 - x1)) by SIN_COS4:18
.= - ((2 * ((sin ((x1 + x0) / 2)) * (sin ((x1 - x0) / 2)))) / (((cos x1) * (cos x0)) * (x0 - x1))) by XCMPLX_1:187 ;
hence  [!sec,x0,x1!] = - (((2 * (sin ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((cos x1) * (cos x0)) * (x0 - x1))) ; ::_thesis: verum
end;