let X be non empty set ; :: thesis: for Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedFunctions X,Y)
for g being bounded Function of X,the carrier of Y st g = f holds
for t being Element of X holds ||.(g . t).|| <= ||.f.||
let Y be RealNormSpace; :: thesis: for f being Point of (R_NormSpace_of_BoundedFunctions X,Y)
for g being bounded Function of X,the carrier of Y st g = f holds
for t being Element of X holds ||.(g . t).|| <= ||.f.||
let f be Point of (R_NormSpace_of_BoundedFunctions X,Y); :: thesis: for g being bounded Function of X,the carrier of Y st g = f holds
for t being Element of X holds ||.(g . t).|| <= ||.f.||
let g be bounded Function of X,the carrier of Y; :: thesis: ( g = f implies for t being Element of X holds ||.(g . t).|| <= ||.f.|| )
assume A1: g = f ; :: thesis: for t being Element of X holds ||.(g . t).|| <= ||.f.||
A2: ( not PreNorms g is empty & PreNorms g is bounded_above ) by Th13;

now

let t be Element of X; :: thesis: ||.(g . t).|| <= ||.f.||
||.(g . t).|| in PreNorms g ;
then ||.(g . t).|| <= sup (PreNorms g) by A2, SEQ_4:def 4;
hence ||.(g . t).|| <= ||.f.|| by A1, Th17; :: thesis: verum

end;

hence for t being Element of X holds ||.(g . t).|| <= ||.f.|| ; :: thesis: verum