begin
theorem Th1:
theorem
theorem Th3:
theorem
theorem Th5:
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!]
theorem Th6:
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!]
theorem
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!])
theorem Th8:
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!]
theorem Th9:
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!]
theorem
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!])
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
([!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:
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!]
theorem Th12:
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!]
theorem
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!])
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
([!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:
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!]
theorem Th15:
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!]
theorem
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!])
theorem
theorem
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!] )
theorem
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!] )
theorem
theorem Th21:
theorem Th22:
for
x0,
x1,
x2,
a,
b being
Real st
x0,
x1,
x2 are_mutually_different holds
[!(AffineMap (a,b)),x0,x1,x2!] = 0
theorem
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
theorem
theorem
theorem
theorem Th27:
theorem Th28:
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
theorem Th29:
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
theorem
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
theorem
theorem
theorem
theorem Th34:
theorem Th35:
theorem Th36:
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))
theorem
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)
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem