let a, b, c, d be Real; :: thesis: for Y being RealBanachSpace

for E being Point of Y

for f being PartFunc of REAL, the carrier of Y st a <= b & c in ['a,b'] & d in ['a,b'] & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds

f /. x = E ) holds

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

let Y be RealBanachSpace; :: thesis: for E being Point of Y

for f being PartFunc of REAL, the carrier of Y st a <= b & c in ['a,b'] & d in ['a,b'] & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds

f /. x = E ) holds

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

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

f /. x = E ) holds

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

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

f /. x = E ) implies integral (f,c,d) = (d - c) * E )

assume that

A1: ( a <= b & c in ['a,b'] & d in ['a,b'] ) and

A3: ( ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds

f /. x = E ) ) ; :: thesis: integral (f,c,d) = (d - c) * E

for E being Point of Y

for f being PartFunc of REAL, the carrier of Y st a <= b & c in ['a,b'] & d in ['a,b'] & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds

f /. x = E ) holds

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

let Y be RealBanachSpace; :: thesis: for E being Point of Y

for f being PartFunc of REAL, the carrier of Y st a <= b & c in ['a,b'] & d in ['a,b'] & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds

f /. x = E ) holds

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

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

f /. x = E ) holds

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

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

f /. x = E ) implies integral (f,c,d) = (d - c) * E )

assume that

A1: ( a <= b & c in ['a,b'] & d in ['a,b'] ) and

A3: ( ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds

f /. x = E ) ) ; :: thesis: integral (f,c,d) = (d - c) * E

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

end;

suppose A5:
c <= d
; :: thesis: integral (f,c,d) = (d - c) * E

then
( c = min (c,d) & d = max (c,d) )
by XXREAL_0:def 9, XXREAL_0:def 10;

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

then ( ['c,d'] c= dom f & ( for x being Real st x in ['c,d'] holds

f /. x = E ) ) by A3;

hence integral (f,c,d) = (d - c) * E by A5, Th1929; :: thesis: verum

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

then ( ['c,d'] c= dom f & ( for x being Real st x in ['c,d'] holds

f /. x = E ) ) by A3;

hence integral (f,c,d) = (d - c) * E by A5, Th1929; :: thesis: verum

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

then
( d = min (c,d) & c = max (c,d) )
by XXREAL_0:def 9, XXREAL_0:def 10;

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

then A10: ( ['d,c'] c= dom f & ( for x being Real st x in ['d,c'] holds

f /. x = E ) ) by A3;

then integral (f,c,d) = - (integral (f,d,c)) by A8, Th1947;

then integral (f,c,d) = - ((c - d) * E) by A8, A10, Th1929;

then integral (f,c,d) = (- (c - d)) * E by RLVECT_1:79;

hence integral (f,c,d) = (d - c) * E ; :: thesis: verum

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

then A10: ( ['d,c'] c= dom f & ( for x being Real st x in ['d,c'] holds

f /. x = E ) ) by A3;

then integral (f,c,d) = - (integral (f,d,c)) by A8, Th1947;

then integral (f,c,d) = - ((c - d) * E) by A8, A10, Th1929;

then integral (f,c,d) = (- (c - d)) * E by RLVECT_1:79;

hence integral (f,c,d) = (d - c) * E ; :: thesis: verum