let X, Y be ComplexNormSpace; :: thesis: ex NORM being Function of (BoundedLinearOperators X,Y),REAL st
for f being set st f in BoundedLinearOperators X,Y holds
NORM . f = upper_bound (PreNorms (modetrans f,X,Y))
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 NORM being Function of (BoundedLinearOperators X,Y),REAL st
for f being set st f in BoundedLinearOperators X,Y holds
NORM . f = upper_bound (PreNorms (modetrans f,X,Y)) ; :: thesis: verum