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

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