let NORM1, NORM2 be Function of (BoundedLinearOperators X,Y),REAL ; :: thesis: ( ( for x being set st x in BoundedLinearOperators X,Y holds
NORM1 . x = sup (PreNorms (modetrans x,X,Y)) ) & ( for x being set st x in BoundedLinearOperators X,Y holds
NORM2 . x = sup (PreNorms (modetrans x,X,Y)) ) implies NORM1 = NORM2 )
assume that
A1: for x being set st x in BoundedLinearOperators X,Y holds
NORM1 . x = sup (PreNorms (modetrans x,X,Y)) and
A2: for x being set st x in BoundedLinearOperators X,Y holds
NORM2 . x = sup (PreNorms (modetrans x,X,Y)) ; :: thesis: NORM1 = NORM2
A3: for z being set st z in BoundedLinearOperators X,Y holds
NORM1 . z = NORM2 . z

proof

let z be set ; :: thesis: ( z in BoundedLinearOperators X,Y implies NORM1 . z = NORM2 . z )
assume A4: z in BoundedLinearOperators X,Y ; :: thesis: NORM1 . z = NORM2 . z
NORM1 . z = sup (PreNorms (modetrans z,X,Y)) by A1, A4;
hence NORM1 . z = NORM2 . z by A2, A4; :: thesis: verum

end;

A5: dom NORM2 = BoundedLinearOperators X,Y by FUNCT_2:def 1;
dom NORM1 = BoundedLinearOperators X,Y by FUNCT_2:def 1;
hence NORM1 = NORM2 by A5, A3, FUNCT_1:9; :: thesis: verum