let a, b, c, d, e be Real; :: thesis: for f being PartFunc of REAL,REAL st a <= b & ( for x being Real st x in ['a,b'] holds

f . x = e ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds

integral (f,c,d) = e * (d - c)

let f be PartFunc of REAL,REAL; :: thesis: ( a <= b & ( for x being Real st x in ['a,b'] holds

f . x = e ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral (f,c,d) = e * (d - c) )

assume that

A1: a <= b and

A2: for x being Real st x in ['a,b'] holds

f . x = e and

A3: ['a,b'] c= dom f and

A4: c in ['a,b'] and

A5: d in ['a,b'] ; :: thesis: integral (f,c,d) = e * (d - c)

A6: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) by A1, A2, A3, Th26;

A7: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;

then A8: c <= b by A4, XXREAL_1:1;

A9: a <= c by A4, A7, XXREAL_1:1;

then A10: ['c,b'] c= ['a,b'] by A8, Lm3;

A11: d <= b by A5, A7, XXREAL_1:1;

A12: a <= d by A5, A7, XXREAL_1:1;

A13: ['a,c'] c= ['a,b'] by A9, A8, Lm3;

f . x = e ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] holds

integral (f,c,d) = e * (d - c)

let f be PartFunc of REAL,REAL; :: thesis: ( a <= b & ( for x being Real st x in ['a,b'] holds

f . x = e ) & ['a,b'] c= dom f & c in ['a,b'] & d in ['a,b'] implies integral (f,c,d) = e * (d - c) )

assume that

A1: a <= b and

A2: for x being Real st x in ['a,b'] holds

f . x = e and

A3: ['a,b'] c= dom f and

A4: c in ['a,b'] and

A5: d in ['a,b'] ; :: thesis: integral (f,c,d) = e * (d - c)

A6: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) by A1, A2, A3, Th26;

A7: ['a,b'] = [.a,b.] by A1, INTEGRA5:def 3;

then A8: c <= b by A4, XXREAL_1:1;

A9: a <= c by A4, A7, XXREAL_1:1;

then A10: ['c,b'] c= ['a,b'] by A8, Lm3;

A11: d <= b by A5, A7, XXREAL_1:1;

A12: a <= d by A5, A7, XXREAL_1:1;

A13: ['a,c'] c= ['a,b'] by A9, A8, Lm3;

per cases
( c <= d or not c <= d )
;

end;

suppose A14:
c <= d
; :: thesis: integral (f,c,d) = e * (d - c)

then
['c,d'] c= ['c,b']
by A11, Lm3;

then ['c,d'] c= ['a,b'] by A10;

then A15: for x being Real st x in ['c,d'] holds

f . x = e by A2;

['c,d'] c= dom f by A3, A9, A11, A6, A14, Th18;

hence integral (f,c,d) = e * (d - c) by A14, A15, Th26; :: thesis: verum

end;then ['c,d'] c= ['a,b'] by A10;

then A15: for x being Real st x in ['c,d'] holds

f . x = e by A2;

['c,d'] c= dom f by A3, A9, A11, A6, A14, Th18;

hence integral (f,c,d) = e * (d - c) by A14, A15, Th26; :: thesis: verum

suppose A16:
not c <= d
; :: thesis: integral (f,c,d) = e * (d - c)

then
['d,c'] c= ['a,c']
by A12, Lm3;

then ['d,c'] c= ['a,b'] by A13;

then A17: for x being Real st x in ['d,c'] holds

f . x = e by A2;

integral (f,c,d) = - (integral (f,['d,c'])) by A16, INTEGRA5:def 4;

then A18: integral (f,c,d) = - (integral (f,d,c)) by A16, INTEGRA5:def 4;

['d,c'] c= dom f by A3, A12, A8, A6, A16, Th18;

then integral (f,d,c) = e * (c - d) by A16, A17, Th26;

hence integral (f,c,d) = e * (d - c) by A18; :: thesis: verum

end;then ['d,c'] c= ['a,b'] by A13;

then A17: for x being Real st x in ['d,c'] holds

f . x = e by A2;

integral (f,c,d) = - (integral (f,['d,c'])) by A16, INTEGRA5:def 4;

then A18: integral (f,c,d) = - (integral (f,d,c)) by A16, INTEGRA5:def 4;

['d,c'] c= dom f by A3, A12, A8, A6, A16, Th18;

then integral (f,d,c) = e * (c - d) by A16, A17, Th26;

hence integral (f,c,d) = e * (d - c) by A18; :: thesis: verum