let X be RealNormSpace; :: thesis: for f being PartFunc of REAL ,the carrier of X
for A being 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 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 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 INTEGRA1:def 1;
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:6;

now

per cases ( b < a or b = a ) by A1, A4, XXREAL_0:1;

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

then integral f,a,b = - (integral f,['b,a']) by Def18;
hence - (integral f,A) = integral f,a,b by A3, A5, INTEGRA5:def 4; :: thesis: verum

end;

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

A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:5;
then ( lower_bound A = b & upper_bound A = a ) by A3, INTEGRA1:6;
then A7: vol A = (upper_bound A) - (upper_bound A) by A6
.= 0 ;
A8: integral f,a,b = integral f,A by A3, A6, th100;
A9: - (integral f,a,b) = - (integral f,A) by A3, A6, th100;
integral f,a,b = 0. X by A7, A3, th46C, A8;
hence - (integral f,A) = integral f,a,b by A9, RLVECT_1:25; :: thesis: verum

end;

end;

end;

hence - (integral f,A) = integral f,a,b ; :: thesis: verum