let f be PartFunc of REAL,REAL; for A being non empty closed_interval Subset of REAL
for a, b being Real st A = [.b,a.] holds
- (integral (f,A)) = integral (f,a,b)
let A be non empty closed_interval Subset of REAL; for a, b being Real st A = [.b,a.] holds
- (integral (f,A)) = integral (f,a,b)
let a, b be Real; ( A = [.b,a.] implies - (integral (f,A)) = integral (f,a,b) )
consider a1, b1 being Real such that
A1:
a1 <= b1
and
A2:
A = [.a1,b1.]
by MEASURE5:14;
assume A3:
A = [.b,a.]
; - (integral (f,A)) = integral (f,a,b)
then A4:
( a1 = b & b1 = a )
by A2, INTEGRA1:5;
now - (integral (f,A)) = integral (f,a,b)per cases
( b < a or b = a )
by A1, A4, XXREAL_0:1;
suppose A6:
b = a
;
- (integral (f,A)) = integral (f,a,b)
A = [.(lower_bound A),(upper_bound A).]
by INTEGRA1:4;
then
(
lower_bound A = b &
upper_bound A = a )
by A3, INTEGRA1:5;
then vol A =
(upper_bound A) - (upper_bound A)
by A6, INTEGRA1:def 5
.=
0
;
then A7:
integral (
f,
A)
= 0
by INTEGRA4:6;
integral (
f,
a,
b)
= integral (
f,
['a,b'])
by A6, Def4;
hence
- (integral (f,A)) = integral (
f,
a,
b)
by A3, A6, A7, Def3;
verum end;
hence
- (integral (f,A)) = integral (f,a,b)
; verum