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