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