let a, b be Real; :: thesis: for Y being RealBanachSpace

for f being PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f holds

integral (f,b,a) = - (integral (f,a,b))

let Y be RealBanachSpace; :: thesis: for f being PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f holds

integral (f,b,a) = - (integral (f,a,b))

let f be PartFunc of REAL, the carrier of Y; :: 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;

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; :: thesis: verum

for f being PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f holds

integral (f,b,a) = - (integral (f,a,b))

let Y be RealBanachSpace; :: thesis: for f being PartFunc of REAL, the carrier of Y st a <= b & ['a,b'] c= dom f holds

integral (f,b,a) = - (integral (f,a,b))

let f be PartFunc of REAL, the carrier of Y; :: 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;

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; :: thesis: verum