let NORM1, NORM2 be Function of (BoundedLinearOperators (X,Y)),REAL; ( ( for x being object st x in BoundedLinearOperators (X,Y) holds
NORM1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being object st x in BoundedLinearOperators (X,Y) holds
NORM2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) implies NORM1 = NORM2 )
assume that
A2:
for x being object st x in BoundedLinearOperators (X,Y) holds
NORM1 . x = upper_bound (PreNorms (modetrans (x,X,Y)))
and
A3:
for x being object st x in BoundedLinearOperators (X,Y) holds
NORM2 . x = upper_bound (PreNorms (modetrans (x,X,Y)))
; NORM1 = NORM2
A4:
for z being object st z in BoundedLinearOperators (X,Y) holds
NORM1 . z = NORM2 . z
A6:
dom NORM2 = BoundedLinearOperators (X,Y)
by FUNCT_2:def 1;
dom NORM1 = BoundedLinearOperators (X,Y)
by FUNCT_2:def 1;
hence
NORM1 = NORM2
by A6, A4; verum