:: 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₄ being Element of REAL n holds
( b₄ = integral (f,A) 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) ) ) );