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