let X be non empty closed_interval Subset of REAL; :: thesis: 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; :: thesis: 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; :: thesis: 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)); :: thesis: 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; :: thesis: ( 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 ) ) ; :: thesis: ||.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

proof

let t be Element of X; :: thesis: ||.(g1 . t).|| <= K
reconsider t1 = t as Real ;
||.(g /. t1).|| <= K by A1;
hence ||.(g1 . t).|| <= K by A2, A1, PARTFUN1:def 6; :: thesis: verum

end;

A4: for x being Element of REAL st x in PreNorms g1 holds
x <= K

proof

let x be Element of REAL ; :: thesis: ( x in PreNorms g1 implies x <= K )
assume x in PreNorms g1 ; :: thesis: x <= K
then consider t being Element of X such that
A5: x = ||.(g1 . t).|| ;
thus x <= K by A3, A5; :: thesis: verum

end;

upper_bound (PreNorms g1) <= K

proof

assume A6: not upper_bound (PreNorms g1) <= K ; :: thesis: contradiction
reconsider s = (upper_bound (PreNorms g1)) - K as Real ;
A7: 0 < s by A6, XREAL_1:50;
( not PreNorms g1 is empty & PreNorms g1 is bounded_above ) by RSSPACE4:11;
then consider r being Real such that
A8: ( r in PreNorms g1 & (upper_bound (PreNorms g1)) - s < r ) by A7, SEQ_4:def 1;
thus contradiction by A8, A4; :: thesis: verum

end;

then ||.v1.|| <= K by A1, RSSPACE4:14;
hence ||.v.|| <= K by FUNCT_1:49; :: thesis: verum