let n be Element of NAT ; 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; 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); 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; ( 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'] )
; integral (f,c,d) = (d - c) * E
A2:
Seg n = dom (integral (f,c,d))
by INTEGR15:def 18;
A3:
now 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 ;
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;
( x in ['a,b'] implies ((proj (i,n)) * f) . x = (proj (i,n)) . E )
assume A5:
x in ['a,b']
;
((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
;
verum
end; hence
integral (
((proj (i,n)) * f),
c,
d)
= ((proj (i,n)) . E) * (d - c)
by A4, A1, INTEGRA6:27;
verum end;
A7:
now for i being Nat st i in dom (integral (f,c,d)) holds
(integral (f,c,d)) . i = ((d - c) * E) . ilet i be
Nat;
( 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))
;
(integral (f,c,d)) . i = ((d - c) * E) . ihence (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
;
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; verum