theorem :: INTEGR15:13

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 g being Function of A,(REAL n) st f | A = g holds

( f is_integrable_on A iff g is integrable )

for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL,(REAL n)

for g being Function of A,(REAL n) st f | A = g holds

( f is_integrable_on A iff g is integrable )