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, INTEGR15:def 15;
then consider r being real number such that
A2: for c being set st c in dom ((proj (i,n)) * f) holds
abs (((proj (i,n)) * f) . c) <= r by RFUNCT_1:72;

now :: thesis: for c being set st c in A /\ (dom ((proj (i,n)) * f)) holds
abs (((proj (i,n)) * f) . c) <= r

let c be set ; :: thesis: ( c in A /\ (dom ((proj (i,n)) * f)) implies abs (((proj (i,n)) * f) . c) <= r )
assume c in A /\ (dom ((proj (i,n)) * f)) ; :: thesis: abs (((proj (i,n)) * f) . c) <= r
then c in dom ((proj (i,n)) * f) by XBOOLE_0:def 4;
hence abs (((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