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
per cases ( c <= d or not c <= d ) ;
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;
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;
end;