deffunc H_{1}( object ) -> object = upper_bound (PreNorms (modetrans ($1,X,Y,Z)));

A1: for z being object st z in BoundedBilinearOperators (X,Y,Z) holds

H_{1}(z) in REAL
by XREAL_0:def 1;

thus ex f being Function of (BoundedBilinearOperators (X,Y,Z)),REAL st

for x being object st x in BoundedBilinearOperators (X,Y,Z) holds

f . x = H_{1}(x)
from FUNCT_2:sch 2(A1); :: thesis: verum

A1: for z being object st z in BoundedBilinearOperators (X,Y,Z) holds

H

thus ex f being Function of (BoundedBilinearOperators (X,Y,Z)),REAL st

for x being object st x in BoundedBilinearOperators (X,Y,Z) holds

f . x = H