let Z be RealNormSpace; :: thesis: for A being non empty closed_interval Subset of REAL
for g being PartFunc of REAL, the carrier of Z st A c= dom g & g | A is bounded holds
||.g.|| | A is bounded
let A be non empty closed_interval Subset of REAL; :: thesis: for g being PartFunc of REAL, the carrier of Z st A c= dom g & g | A is bounded holds
||.g.|| | A is bounded
let g be PartFunc of REAL, the carrier of Z; :: thesis: ( A c= dom g & g | A is bounded implies ||.g.|| | A is bounded )
assume A1: ( A c= dom g & g | A is bounded ) ; :: thesis: ||.g.|| | A is bounded
then A2: ||.(g | A).|| = ||.g.|| | A by Th1918;
reconsider h = g | A as Function of A, the carrier of Z by A1, Lm3;
h is bounded by A1;
hence ||.g.|| | A is bounded by A2, Th1914; :: thesis: verum