:: deftheorem Def17 defines integral INTEGR15:def 17 :

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL,(REAL n)

for b_{4} being Element of REAL n holds

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

b_{4} . i = integral (((proj (i,n)) * f),A) ) ) );

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL,(REAL n)

for b

( b

b