let n be Element of NAT ; :: thesis: for A being non empty closed_interval Subset of REAL

for f being PartFunc of REAL,(REAL n) st f is bounded & A c= dom f holds

f | A is bounded

let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of REAL,(REAL n) st f is bounded & A c= dom f holds

f | A is bounded

let f be PartFunc of REAL,(REAL n); :: thesis: ( f is bounded & A c= dom f implies f | A is bounded )

assume A1: ( f is bounded & A c= dom f ) ; :: thesis: f | A is bounded

let i be Element of NAT ; :: according to INTEGR15:def 15 :: thesis: ( not i in Seg n or (proj (i,n)) * (f | A) is bounded )

set P = proj (i,n);

assume i in Seg n ; :: thesis: (proj (i,n)) * (f | A) is bounded

then (proj (i,n)) * f is bounded by A1;

then consider r being Real such that

A2: for c being object st c in dom ((proj (i,n)) * f) holds

|.(((proj (i,n)) * f) . c).| <= r by RFUNCT_1:72;

hence (proj (i,n)) * (f | A) is bounded by RELAT_1:83; :: thesis: verum

for f being PartFunc of REAL,(REAL n) st f is bounded & A c= dom f holds

f | A is bounded

let A be non empty closed_interval Subset of REAL; :: thesis: for f being PartFunc of REAL,(REAL n) st f is bounded & A c= dom f holds

f | A is bounded

let f be PartFunc of REAL,(REAL n); :: thesis: ( f is bounded & A c= dom f implies f | A is bounded )

assume A1: ( f is bounded & A c= dom f ) ; :: thesis: f | A is bounded

let i be Element of NAT ; :: according to INTEGR15:def 15 :: thesis: ( not i in Seg n or (proj (i,n)) * (f | A) is bounded )

set P = proj (i,n);

assume i in Seg n ; :: thesis: (proj (i,n)) * (f | A) is bounded

then (proj (i,n)) * f is bounded by A1;

then consider r being Real such that

A2: for c being object st c in dom ((proj (i,n)) * f) holds

|.(((proj (i,n)) * f) . c).| <= r by RFUNCT_1:72;

now :: thesis: for c being object st c in A /\ (dom ((proj (i,n)) * f)) holds

|.(((proj (i,n)) * f) . c).| <= r

then
((proj (i,n)) * f) | A is bounded
by RFUNCT_1:73;|.(((proj (i,n)) * f) . c).| <= r

let c be object ; :: thesis: ( c in A /\ (dom ((proj (i,n)) * f)) implies |.(((proj (i,n)) * f) . c).| <= r )

assume c in A /\ (dom ((proj (i,n)) * f)) ; :: thesis: |.(((proj (i,n)) * f) . c).| <= r

then c in dom ((proj (i,n)) * f) by XBOOLE_0:def 4;

hence |.(((proj (i,n)) * f) . c).| <= r by A2; :: thesis: verum

end;assume c in A /\ (dom ((proj (i,n)) * f)) ; :: thesis: |.(((proj (i,n)) * f) . c).| <= r

then c in dom ((proj (i,n)) * f) by XBOOLE_0:def 4;

hence |.(((proj (i,n)) * f) . c).| <= r by A2; :: thesis: verum

hence (proj (i,n)) * (f | A) is bounded by RELAT_1:83; :: thesis: verum