let X be non empty set ; :: thesis: for Y being ComplexNormSpace
for f being Point of (C_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 ComplexNormSpace; :: thesis: for f being Point of (C_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 (C_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 Th12;

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

let t be Element of X; :: thesis: ||.(g . t).|| <= ||.f.||
||.(g . t).|| in PreNorms g ;
then ||.(g . t).|| <= upper_bound (PreNorms g) by A2, SEQ_4:def 1;
then ||.(g . t).|| <= (ComplexBoundedFunctionsNorm (X,Y)) . g by Th15;
hence ||.(g . t).|| <= ||.f.|| by A1; :: thesis: verum

end;

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