let X be non empty closed_interval Subset of REAL; :: thesis: for Y being RealNormSpace
for v being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for g being PartFunc of REAL,Y st g = v holds
for t being Real st t in X holds
||.(g /. t).|| <= ||.v.||
let Y be RealNormSpace; :: thesis: for v being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for g being PartFunc of REAL,Y st g = v holds
for t being Real st t in X holds
||.(g /. t).|| <= ||.v.||
let v be Point of (R_NormSpace_of_ContinuousFunctions (X,Y)); :: thesis: for g being PartFunc of REAL,Y st g = v holds
for t being Real st t in X holds
||.(g /. t).|| <= ||.v.||
let g be PartFunc of REAL,Y; :: thesis: ( g = v implies for t being Real st t in X holds
||.(g /. t).|| <= ||.v.|| )
assume A1: g = v ; :: thesis: for t being Real st t in X holds
||.(g /. t).|| <= ||.v.||
consider f being continuous PartFunc of REAL,Y such that
A2: ( v = f & dom f = X ) by Def2;
reconsider g1 = g as bounded Function of X,Y by A1, Th9, A2;
reconsider v1 = v as VECTOR of (R_NormSpace_of_BoundedFunctions (X,Y)) by TARSKI:def 3;
A3: ||.v1.|| = ||.v.|| by FUNCT_1:49;
let t be Real; :: thesis: ( t in X implies ||.(g /. t).|| <= ||.v.|| )
assume t in X ; :: thesis: ||.(g /. t).|| <= ||.v.||
then reconsider t1 = t as Element of X ;
||.(g1 . t1).|| <= ||.v1.|| by A1, RSSPACE4:16;
hence ||.(g /. t).|| <= ||.v.|| by A2, A1, PARTFUN1:def 6, A3; :: thesis: verum