:: deftheorem defines is_integrable_on INTEGR15:def 16 :

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL,(REAL n) holds

( f is_integrable_on A iff for i being Element of NAT st i in Seg n holds

(proj (i,n)) * f is_integrable_on 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) holds

( f is_integrable_on A iff for i being Element of NAT st i in Seg n holds

(proj (i,n)) * f is_integrable_on A );