let n be Element of NAT ; :: thesis: for b, a being real number
for f being PartFunc of REAL,(REAL n) holds integral (f,b,a) = - (integral (f,a,b))
let b, a be real number ; :: thesis: for f being PartFunc of REAL,(REAL n) holds integral (f,b,a) = - (integral (f,a,b))
let f be PartFunc of REAL,(REAL n); :: thesis: integral (f,b,a) = - (integral (f,a,b))
A1: ( a is Real & b is Real ) by XREAL_0:def 1;

per cases ( a <= b or not a <= b ) ;

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

then A2: ['a,b'] = [.a,b.] by INTEGRA5:def 3;
integral (f,['a,b']) = integral (f,a,b) by A1, A2, INTEGR15:19;
hence integral (f,b,a) = - (integral (f,a,b)) by A1, A2, INTEGR15:20; :: thesis: verum

end;

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

then A3: ['b,a'] = [.b,a.] by INTEGRA5:def 3;
then - (integral (f,['b,a'])) = integral (f,a,b) by A1, INTEGR15:20;
hence integral (f,b,a) = - (integral (f,a,b)) by A1, A3, INTEGR15:19; :: thesis: verum

end;

end;