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

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