:: 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 );

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 );