let X be non empty closed_interval Subset of REAL; for Y being RealNormSpace
for K being Real
for v being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for g being PartFunc of REAL,Y st g = v & ( for t being Real st t in X holds
||.(g /. t).|| <= K ) holds
||.v.|| <= K
let Y be RealNormSpace; for K being Real
for v being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for g being PartFunc of REAL,Y st g = v & ( for t being Real st t in X holds
||.(g /. t).|| <= K ) holds
||.v.|| <= K
let K be Real; for v being Point of (R_NormSpace_of_ContinuousFunctions (X,Y))
for g being PartFunc of REAL,Y st g = v & ( for t being Real st t in X holds
||.(g /. t).|| <= K ) holds
||.v.|| <= K
let v be Point of (R_NormSpace_of_ContinuousFunctions (X,Y)); for g being PartFunc of REAL,Y st g = v & ( for t being Real st t in X holds
||.(g /. t).|| <= K ) holds
||.v.|| <= K
let g be PartFunc of REAL,Y; ( g = v & ( for t being Real st t in X holds
||.(g /. t).|| <= K ) implies ||.v.|| <= K )
assume A1:
( g = v & ( for t being Real st t in X holds
||.(g /. t).|| <= K ) )
; ||.v.|| <= K
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:
for t being Element of X holds ||.(g1 . t).|| <= K
A4:
for x being Element of REAL st x in PreNorms g1 holds
x <= K
upper_bound (PreNorms g1) <= K
then
||.v1.|| <= K
by A1, RSSPACE4:14;
hence
||.v.|| <= K
by FUNCT_1:49; verum