let f be PartFunc of REAL ,REAL ; :: thesis: for A being 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 closed-interval Subset of REAL ; :: thesis: for a, b being Real st A = [.b,a.] holds
- (integral f,A) = integral f,a,b
let a, b be Real; :: thesis: ( A = [.b,a.] implies - (integral f,A) = integral f,a,b )
assume A1: A = [.b,a.] ; :: thesis: - (integral f,A) = integral f,a,b
consider a1, b1 being Real such that
A2: ( a1 <= b1 & A = [.a1,b1.] ) by INTEGRA1:def 1;
A3: ( a1 = b & b1 = a ) by A1, A2, INTEGRA1:6;

now

per cases ( b < a or b = a ) by A2, A3, XXREAL_0:1;

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

then integral f,a,b = - (integral f,['b,a']) by Def5;
hence - (integral f,A) = integral f,a,b by A1, A4, Def4; :: thesis: verum

end;

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

then A6: integral f,a,b = integral f,['a,b'] by Def5;
A = [.(inf A),(sup A).] by INTEGRA1:5;
then ( inf A = b & sup A = a ) by A1, INTEGRA1:6;
then vol A = (sup A) - (sup A) by A5, INTEGRA1:def 6
.= 0 ;
then integral f,A = 0 by INTEGRA4:6;
hence - (integral f,A) = integral f,a,b by A1, A5, A6, Def4; :: thesis: verum

end;

end;

end;

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