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 ;
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 ;
((proj (i,n)) * f) . x = (proj (i,n)) . (f /. x) by
.= (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 ; :: 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
.= ((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 ; :: thesis: verum