let n be Element of NAT ; :: thesis: for a, b being real number
for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f holds
integral (f,b,a) = - (integral (f,a,b))
let a, b be real number ; :: thesis: for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f holds
integral (f,b,a) = - (integral (f,a,b))
let f be PartFunc of REAL,(REAL-NS n); :: thesis: ( a <= b & ['a,b'] c= dom f implies integral (f,b,a) = - (integral (f,a,b)) )
assume A1: ( a <= b & ['a,b'] c= dom f ) ; :: thesis: integral (f,b,a) = - (integral (f,a,b))
then A2: ['a,b'] = [.a,b.] by INTEGRA5:def 3;
A3: ( a is Real & b is Real ) by XREAL_0:def 1;
then integral (f,['a,b']) = integral (f,a,b) by A2, INTEGR18:16;
hence integral (f,b,a) = - (integral (f,a,b)) by A3, A2, A1, INTEGR18:18; :: thesis: verum