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;
now :: thesis: for c being object st c in A /\ (dom ((proj (i,n)) * f)) holds
|.(((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;
then ((proj (i,n)) * f) | A is bounded by RFUNCT_1:73;
hence (proj (i,n)) * (f | A) is bounded by RELAT_1:83; :: thesis: verum