let NORM1, NORM2 be Function of (BoundedBilinearOperators (X,Y,Z)),REAL; :: thesis: ( ( for x being object st x in BoundedBilinearOperators (X,Y,Z) holds
NORM1 . x = upper_bound (PreNorms (modetrans (x,X,Y,Z))) ) & ( for x being object st x in BoundedBilinearOperators (X,Y,Z) holds
NORM2 . x = upper_bound (PreNorms (modetrans (x,X,Y,Z))) ) implies NORM1 = NORM2 )
assume that
A2: for x being object st x in BoundedBilinearOperators (X,Y,Z) holds
NORM1 . x = upper_bound (PreNorms (modetrans (x,X,Y,Z))) and
A3: for x being object st x in BoundedBilinearOperators (X,Y,Z) holds
NORM2 . x = upper_bound (PreNorms (modetrans (x,X,Y,Z))) ; :: thesis: NORM1 = NORM2
A4: for z being object st z in BoundedBilinearOperators (X,Y,Z) holds
NORM1 . z = NORM2 . z

proof

let z be object ; :: thesis: ( z in BoundedBilinearOperators (X,Y,Z) implies NORM1 . z = NORM2 . z )
assume A5: z in BoundedBilinearOperators (X,Y,Z) ; :: thesis: NORM1 . z = NORM2 . z
NORM1 . z = upper_bound (PreNorms (modetrans (z,X,Y,Z))) by A2, A5;
hence NORM1 . z = NORM2 . z by A3, A5; :: thesis: verum

end;

dom NORM1 = BoundedBilinearOperators (X,Y,Z) by FUNCT_2:def 1;
hence NORM1 = NORM2 by A4, FUNCT_2:def 1; :: thesis: verum