let n be non zero Element of NAT ; :: thesis: for a, b being Real
for g being continuous PartFunc of REAL,(REAL n) st dom g = ['a,b'] holds
g is_integrable_on ['a,b']
let a, b be Real; :: thesis: for g being continuous PartFunc of REAL,(REAL n) st dom g = ['a,b'] holds
g is_integrable_on ['a,b']
let g be continuous PartFunc of REAL,(REAL n); :: thesis: ( dom g = ['a,b'] implies g is_integrable_on ['a,b'] )
assume A1: dom g = ['a,b'] ; :: thesis: g is_integrable_on ['a,b']
let i be Element of NAT ; :: according to INTEGR15:def 16 :: thesis: ( not i in Seg n or (proj (i,n)) * g is_integrable_on ['a,b'] )
assume i in Seg n ; :: thesis: (proj (i,n)) * g is_integrable_on ['a,b']
then A2: (proj (i,n)) * g is continuous by NFCONT_4:44;
dom (proj (i,n)) = REAL n by FUNCT_2:def 1;
then rng g c= dom (proj (i,n)) ;
then A3: ['a,b'] c= dom ((proj (i,n)) * g) by A1, RELAT_1:27;
((proj (i,n)) * g) | ['a,b'] is continuous by A2;
hence (proj (i,n)) * g is_integrable_on ['a,b'] by A3, INTEGRA5:11; :: thesis: verum