let n be Element of NAT ; :: thesis: for a, b, c, d being Real

for E being Point of (REAL-NS n)

for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds

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

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

let a, b, c, d be Real; :: thesis: for E being Point of (REAL-NS n)

for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds

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

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

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

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

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

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

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

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

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

reconsider f1 = f as PartFunc of REAL,(REAL n) by REAL_NS1:def 4;

reconsider e1 = e as Element of REAL n by REAL_NS1:def 4;

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

f1 . x = e1 by A1;

A3: ( f1 is_integrable_on ['a,b'] & f1 | ['a,b'] is bounded & integral (f1,a,b) = (b - a) * e1 ) by Th29, A1, A2;

A4: integral (f1,c,d) = (d - c) * e1 by Th30, A1;

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

then A5: ( a <= c & d <= b & a <= d & c <= b ) by A1, XXREAL_1:1;

for E being Point of (REAL-NS n)

for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds

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

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

let a, b, c, d be Real; :: thesis: for E being Point of (REAL-NS n)

for f being PartFunc of REAL,(REAL-NS n) st a <= b & ['a,b'] c= dom f & ( for x being Real st x in ['a,b'] holds

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

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

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

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

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

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

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

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

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

reconsider f1 = f as PartFunc of REAL,(REAL n) by REAL_NS1:def 4;

reconsider e1 = e as Element of REAL n by REAL_NS1:def 4;

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

f1 . x = e1 by A1;

A3: ( f1 is_integrable_on ['a,b'] & f1 | ['a,b'] is bounded & integral (f1,a,b) = (b - a) * e1 ) by Th29, A1, A2;

A4: integral (f1,c,d) = (d - c) * e1 by Th30, A1;

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

then A5: ( a <= c & d <= b & a <= d & c <= b ) by A1, XXREAL_1:1;

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

end;

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

A7:
( ['c,d'] c= dom f1 & f1 | ['c,d'] is bounded & f1 is_integrable_on ['c,d'] )
by A3, A1, Th9, A5, A6, Th2;

integral (f1,c,d) = integral (f,c,d) by A7, A6, Th45;

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

end;integral (f1,c,d) = integral (f,c,d) by A7, A6, Th45;

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

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

A9:
( ['d,c'] c= dom f1 & f1 | ['d,c'] is bounded & f1 is_integrable_on ['d,c'] )
by A3, A1, Th9, A5, A8, Th2;

A10: integral (f1,d,c) = integral (f,d,c) by A9, A8, Th45;

integral (f1,c,d) = - (integral (f1,d,c)) by Th33

.= - (integral (f,d,c)) by A10, REAL_NS1:4

.= integral (f,c,d) by A8, A9, Th47 ;

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

end;A10: integral (f1,d,c) = integral (f,d,c) by A9, A8, Th45;

integral (f1,c,d) = - (integral (f1,d,c)) by Th33

.= - (integral (f,d,c)) by A10, REAL_NS1:4

.= integral (f,c,d) by A8, A9, Th47 ;

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