let a, b, c, d be Real; :: thesis: for Y being RealBanachSpace
for f being continuous PartFunc of REAL, the carrier of Y st a <= b & c <= d & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))
let Y be RealBanachSpace; :: thesis: for f being continuous PartFunc of REAL, the carrier of Y st a <= b & c <= d & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds
integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))
let f be continuous PartFunc of REAL, the carrier of Y; :: thesis: ( a <= b & c <= d & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) )
assume A1: ( a <= b & c <= d & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] ) ; :: thesis: integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d))
['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;
then A2: ( a <= c & c <= b & a <= d & d <= b ) by A1, XXREAL_1:1;
then A3: ( ['a,d'] c= ['a,b'] & c in ['a,d'] ) by A1, INTEGR19:1;
then ['a,d'] c= dom f by A1;
hence integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) by A2, A3, Th1908; :: thesis: verum