let X be set ; :: thesis: for S being RealNormSpace
for f, g being PartFunc of S,RNS_Real st f is_continuous_on X & g = ||.f.|| holds
g is_continuous_on X
let S be RealNormSpace; :: thesis: for f, g being PartFunc of S,RNS_Real st f is_continuous_on X & g = ||.f.|| holds
g is_continuous_on X
let f, g be PartFunc of S,RNS_Real; :: thesis: ( f is_continuous_on X & g = ||.f.|| implies g is_continuous_on X )
assume that
A1: f is_continuous_on X and
A2: g = ||.f.|| ; :: thesis: g is_continuous_on X
||.(f | X).|| = g | X by A2, NFCONT_1:35;
hence g is_continuous_on X by A1, A2, Th21, NORMSP_0:def 2; :: thesis: verum