let n be non zero Element of NAT ; 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; 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); ( dom g = ['a,b'] implies g | ['a,b'] is bounded )
assume A1:
dom g = ['a,b']
; 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
let i be Element of NAT ; INTEGR15:def 15 ( not i in Seg n or (proj (i,n)) * (g | ['a,b']) is bounded )
assume A3:
i in Seg n
; (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; verum