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 )
consider a1, b1 being Real such that
A1: a1 <= b1 and
A2: A = [.a1,b1.] by INTEGRA1:def 1;
assume A3: A = [.b,a.] ; :: 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 Def5;
hence - (integral f,A) = integral f,a,b by A3, A5, Def4; :: thesis: verum

end;

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

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

end;

end;

end;

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