let A be non empty closed_interval Subset of REAL; :: thesis: for n being non zero Element of NAT
for h being PartFunc of REAL,(REAL n) st A c= dom h & h | A is bounded holds
|.h.| | A is bounded
let n be non zero Element of NAT ; :: thesis: for h being PartFunc of REAL,(REAL n) st A c= dom h & h | A is bounded holds
|.h.| | A is bounded
let h be PartFunc of REAL,(REAL n); :: thesis: ( A c= dom h & h | A is bounded implies |.h.| | A is bounded )
assume A1: ( A c= dom h & h | A is bounded ) ; :: thesis: |.h.| | A is bounded
A2: |.(h | A).| = |.h.| | A by Th18, A1;
reconsider g = h | A as Function of A,(REAL n) by A1, Lm9;
g is bounded by A1;
then |.g.| is bounded by Th14;
hence |.h.| | A is bounded by A2, Th17; :: thesis: verum