let a, b, c, d, e be Real; 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; ( 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']
; 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 )
;
suppose A14:
c <= d
;
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;
verum end; suppose A16:
not
c <= d
;
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;
verum end;