:: deftheorem defines integrable INTEGR15:def 13 :
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n) holds
( f is integrable iff for i being Element of NAT st i in Seg n holds
(proj (i,n)) * f is integrable );