let NORM1, NORM2 be Function of (ComplexBoundedFunctions (X,Y)),REAL; :: thesis: ( ( for x being object st x in ComplexBoundedFunctions (X,Y) holds

NORM1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being object st x in ComplexBoundedFunctions (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 ComplexBoundedFunctions (X,Y) holds

NORM1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) and

A3: for x being object st x in ComplexBoundedFunctions (X,Y) holds

NORM2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ; :: thesis: NORM1 = NORM2

A4: for z being object st z in ComplexBoundedFunctions (X,Y) holds

NORM1 . z = NORM2 . z

hence NORM1 = NORM2 by A4, FUNCT_1:2; :: thesis: verum

NORM1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ) & ( for x being object st x in ComplexBoundedFunctions (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 ComplexBoundedFunctions (X,Y) holds

NORM1 . x = upper_bound (PreNorms (modetrans (x,X,Y))) and

A3: for x being object st x in ComplexBoundedFunctions (X,Y) holds

NORM2 . x = upper_bound (PreNorms (modetrans (x,X,Y))) ; :: thesis: NORM1 = NORM2

A4: for z being object st z in ComplexBoundedFunctions (X,Y) holds

NORM1 . z = NORM2 . z

proof

( dom NORM1 = ComplexBoundedFunctions (X,Y) & dom NORM2 = ComplexBoundedFunctions (X,Y) )
by FUNCT_2:def 1;
let z be object ; :: thesis: ( z in ComplexBoundedFunctions (X,Y) implies NORM1 . z = NORM2 . z )

assume A5: z in ComplexBoundedFunctions (X,Y) ; :: thesis: NORM1 . z = NORM2 . z

NORM1 . z = upper_bound (PreNorms (modetrans (z,X,Y))) by A2, A5;

hence NORM1 . z = NORM2 . z by A3, A5; :: thesis: verum

end;assume A5: z in ComplexBoundedFunctions (X,Y) ; :: thesis: NORM1 . z = NORM2 . z

NORM1 . z = upper_bound (PreNorms (modetrans (z,X,Y))) by A2, A5;

hence NORM1 . z = NORM2 . z by A3, A5; :: thesis: verum

hence NORM1 = NORM2 by A4, FUNCT_1:2; :: thesis: verum