let X be non empty set ; :: thesis: ex NORM being Function of (BoundedFunctions X),REAL st
for F being set st F in BoundedFunctions X holds
NORM . F = upper_bound (PreNorms (modetrans (F,X)))
deffunc H₁( set ) -> Element of REAL = upper_bound (PreNorms (modetrans ($1,X)));
A1: for z being set st z in BoundedFunctions X holds
H₁(z) in REAL ;
ex f being Function of (BoundedFunctions X),REAL st
for x being set st x in BoundedFunctions X holds
f . x = H₁(x) from FUNCT_2:sch 2(A1);
hence ex NORM being Function of (BoundedFunctions X),REAL st
for F being set st F in BoundedFunctions X holds
NORM . F = upper_bound (PreNorms (modetrans (F,X))) ; :: thesis: verum