let X be RealNormSpace; :: thesis: for f being PartFunc of REAL, the carrier of X

for A being non empty closed_interval Subset of REAL

for a, b being Real st A = [.b,a.] & A c= dom f holds

- (integral (f,A)) = integral (f,a,b)

let f be PartFunc of REAL, the carrier of X; :: thesis: for A being non empty closed_interval Subset of REAL

for a, b being Real st A = [.b,a.] & A c= dom f holds

- (integral (f,A)) = integral (f,a,b)

let A be non empty closed_interval Subset of REAL; :: thesis: for a, b being Real st A = [.b,a.] & A c= dom f holds

- (integral (f,A)) = integral (f,a,b)

let a, b be Real; :: thesis: ( A = [.b,a.] & A c= dom f 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.] & A c= dom f ) ; :: thesis: - (integral (f,A)) = integral (f,a,b)

then A4: ( a1 = b & b1 = a ) by A2, INTEGRA1:5;

for A being non empty closed_interval Subset of REAL

for a, b being Real st A = [.b,a.] & A c= dom f holds

- (integral (f,A)) = integral (f,a,b)

let f be PartFunc of REAL, the carrier of X; :: thesis: for A being non empty closed_interval Subset of REAL

for a, b being Real st A = [.b,a.] & A c= dom f holds

- (integral (f,A)) = integral (f,a,b)

let A be non empty closed_interval Subset of REAL; :: thesis: for a, b being Real st A = [.b,a.] & A c= dom f holds

- (integral (f,A)) = integral (f,a,b)

let a, b be Real; :: thesis: ( A = [.b,a.] & A c= dom f 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.] & A c= dom f ) ; :: thesis: - (integral (f,A)) = integral (f,a,b)

then A4: ( a1 = b & b1 = a ) by A2, INTEGRA1:5;

now :: thesis: - (integral (f,A)) = integral (f,a,b)end;

hence
- (integral (f,A)) = integral (f,a,b)
; :: thesis: verumper cases
( b < a or b = a )
by A1, A4, XXREAL_0:1;

end;

suppose A5:
b < a
; :: thesis: - (integral (f,A)) = integral (f,a,b)

then
integral (f,a,b) = - (integral (f,['b,a']))
by Def9;

hence - (integral (f,A)) = integral (f,a,b) by A3, A5, INTEGRA5:def 3; :: thesis: verum

end;hence - (integral (f,A)) = integral (f,a,b) by A3, A5, INTEGRA5:def 3; :: thesis: verum

suppose A6:
b = a
; :: thesis: - (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 A7: vol A = (upper_bound A) - (upper_bound A) by A6

.= 0 ;

A8: integral (f,a,b) = integral (f,A) by A3, A6, Th16;

A9: - (integral (f,a,b)) = - (integral (f,A)) by A3, A6, Th16;

integral (f,a,b) = 0. X by A7, A3, Th17, A8;

hence - (integral (f,A)) = integral (f,a,b) by A9, RLVECT_1:12; :: thesis: verum

end;then ( lower_bound A = b & upper_bound A = a ) by A3, INTEGRA1:5;

then A7: vol A = (upper_bound A) - (upper_bound A) by A6

.= 0 ;

A8: integral (f,a,b) = integral (f,A) by A3, A6, Th16;

A9: - (integral (f,a,b)) = - (integral (f,A)) by A3, A6, Th16;

integral (f,a,b) = 0. X by A7, A3, Th17, A8;

hence - (integral (f,A)) = integral (f,a,b) by A9, RLVECT_1:12; :: thesis: verum