let n be non zero Element of NAT ; :: thesis: for a, b being Real
for f being continuous PartFunc of REAL,(REAL-NS n) st dom f = ['a,b'] holds
f is_integrable_on ['a,b']
let a, b be Real; :: thesis: for f being continuous PartFunc of REAL,(REAL-NS n) st dom f = ['a,b'] holds
f is_integrable_on ['a,b']
let f be continuous PartFunc of REAL,(REAL-NS n); :: thesis: ( dom f = ['a,b'] implies f is_integrable_on ['a,b'] )
assume A1: dom f = ['a,b'] ; :: thesis: f is_integrable_on ['a,b']
reconsider g = f as PartFunc of REAL,(REAL n) by REAL_NS1:def 4;
A2: g is continuous by NFCONT_4:23;
then A3: g is_integrable_on ['a,b'] by A1, Th30;
g | ['a,b'] is bounded by A2, A1, Th29;
hence f is_integrable_on ['a,b'] by A1, A3, INTEGR19:44; :: thesis: verum