let n be Element of NAT ; :: thesis: for a, b, c, d being Real
for f being PartFunc of REAL,(REAL n)
for E being Element of REAL n 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) = (d - c) * E
let a, b, c, d be Real; :: thesis: for f being PartFunc of REAL,(REAL n)
for E being Element of REAL n 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) = (d - c) * E
let f be PartFunc of REAL,(REAL n); :: thesis: for E being Element of REAL n 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) = (d - c) * E
let E be Element of REAL n; :: 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) = (d - c) * E )
assume A1: ( 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'] ) ; :: thesis: integral (f,c,d) = (d - c) * E
A2: Seg n = dom (integral (f,c,d)) by INTEGR15:def 18;

A3: now :: thesis: for i being Element of NAT holds integral (((proj (i,n)) * f),c,d) = ((proj (i,n)) . E) * (d - c)

let i be Element of NAT ; :: thesis: integral (((proj (i,n)) * f),c,d) = ((proj (i,n)) . E) * (d - c)
set P = proj (i,n);
dom (proj (i,n)) = REAL n by FUNCT_2:def 1;
then rng f c= dom (proj (i,n)) ;
then A4: ['a,b'] c= dom ((proj (i,n)) * f) by A1, RELAT_1:27;
for x being Real st x in ['a,b'] holds
((proj (i,n)) * f) . x = (proj (i,n)) . E

proof

let x be Real; :: thesis: ( x in ['a,b'] implies ((proj (i,n)) * f) . x = (proj (i,n)) . E )
assume A5: x in ['a,b'] ; :: thesis: ((proj (i,n)) * f) . x = (proj (i,n)) . E
then A6: f . x = f /. x by A1, PARTFUN1:def 6;
((proj (i,n)) * f) . x = (proj (i,n)) . (f /. x) by A4, A5, A6, FUNCT_1:12
.= (proj (i,n)) . E by A6, A5, A1 ;
hence ((proj (i,n)) * f) . x = (proj (i,n)) . E ; :: thesis: verum

end;

hence integral (((proj (i,n)) * f),c,d) = ((proj (i,n)) . E) * (d - c) by A4, A1, INTEGRA6:27; :: thesis: verum

end;

A7: now :: thesis: for i being Nat st i in dom (integral (f,c,d)) holds
(integral (f,c,d)) . i = ((d - c) * E) . i

let i be Nat; :: thesis: ( i in dom (integral (f,c,d)) implies (integral (f,c,d)) . i = ((d - c) * E) . i )
set P = proj (i,n);
assume A8: i in dom (integral (f,c,d)) ; :: thesis: (integral (f,c,d)) . i = ((d - c) * E) . i
hence (integral (f,c,d)) . i = integral (((proj (i,n)) * f),c,d) by A2, INTEGR15:def 18
.= ((proj (i,n)) . E) * (d - c) by A3, A8
.= (d - c) * (E . i) by PDIFF_1:def 1
.= ((d - c) * E) . i by RVSUM_1:44 ;
:: thesis: verum

end;

len ((d - c) * E) = n by CARD_1:def 7;
then Seg n = dom ((d - c) * E) by FINSEQ_1:def 3;
hence integral (f,c,d) = (d - c) * E by A2, A7, FINSEQ_1:13; :: thesis: verum