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 | ['a,b'] is bounded
let a, b be Real; :: thesis: for g being continuous PartFunc of REAL,(REAL n) st dom g = ['a,b'] holds
g | ['a,b'] is bounded
let g be continuous PartFunc of REAL,(REAL n); :: thesis: ( dom g = ['a,b'] implies g | ['a,b'] is bounded )
assume A1: dom g = ['a,b'] ; :: thesis: g | ['a,b'] is bounded
A2: for i being Element of NAT st i in Seg n holds
((proj (i,n)) * g) | ['a,b'] is continuous

proof

let i be Element of NAT ; :: thesis: ( i in Seg n implies ((proj (i,n)) * g) | ['a,b'] is continuous )
assume i in Seg n ; :: thesis: ((proj (i,n)) * g) | ['a,b'] is continuous
then (proj (i,n)) * g is continuous by NFCONT_4:44;
hence ((proj (i,n)) * g) | ['a,b'] is continuous ; :: thesis: verum

end;

let i be Element of NAT ; :: according to INTEGR15:def 15 :: thesis: ( not i in Seg n or (proj (i,n)) * (g | ['a,b']) is bounded )
assume A3: i in Seg n ; :: thesis: (proj (i,n)) * (g | ['a,b']) is bounded
dom (proj (i,n)) = REAL n by FUNCT_2:def 1;
then rng g c= dom (proj (i,n)) ;
then ['a,b'] c= dom ((proj (i,n)) * g) by A1, RELAT_1:27;
then ((proj (i,n)) * g) | ['a,b'] is bounded by A3, A2, INTEGRA5:10;
hence (proj (i,n)) * (g | ['a,b']) is bounded by Th28; :: thesis: verum