:: 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₅ being Element of REAL n holds
( b₅ = integral (f,a,b) iff ( dom b₅ = Seg n & ( for i being Element of NAT st i in Seg n holds
b₅ . i = integral (((proj (i,n)) * f),a,b) ) ) );