deffunc H₁( object ) -> object = upper_bound (PreNorms (Bound2Lipschitz ($1,X)));
A1: for z being object st z in BoundedLinearFunctionals X holds
H₁(z) in REAL by XREAL_0:def 1;
thus ex f being Function of (BoundedLinearFunctionals X),REAL st
for x being object st x in BoundedLinearFunctionals X holds
f . x = H₁(x) from FUNCT_2:sch 2(A1); :: thesis: verum