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 ;
then A2: ( a <= c & c <= b & a <= d & d <= b ) by ;
then A3: ( ['a,d'] c= ['a,b'] & c in ['a,d'] ) by ;
then ['a,d'] c= dom f by A1;
hence integral (f,a,d) = (integral (f,a,c)) + (integral (f,c,d)) by ; :: thesis: verum