deffunc H₁( object ) -> object = upper_bound (PreNorms (modetrans ($1,X,Y,Z)));
A1: for z being object st z in BoundedBilinearOperators (X,Y,Z) holds
H₁(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₁(x) from FUNCT_2:sch 2(A1); :: thesis: verum