let n be Element of NAT ; for a, b being Real
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; 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); ( 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 )
; 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 A2, INTEGR18:16;
hence
integral (f,b,a) = - (integral (f,a,b))
by A2, A1, INTEGR18:18; verum