:: deftheorem Def18 defines integral INTEGR15:def 18 :

for a, b being Real

for n being Element of NAT

for f being PartFunc of REAL,(REAL n)

for b_{5} being Element of REAL n holds

( b_{5} = integral (f,a,b) iff ( dom b_{5} = Seg n & ( for i being Element of NAT st i in Seg n holds

b_{5} . i = integral (((proj (i,n)) * f),a,b) ) ) );

for a, b being Real

for n being Element of NAT

for f being PartFunc of REAL,(REAL n)

for b

( b

b