let NORM1, NORM2 be Function of (ComplexBoundedFunctions X),REAL; :: thesis: ( ( for x being set st x in ComplexBoundedFunctions X holds
NORM1 . x = upper_bound (PreNorms (modetrans (x,X))) ) & ( for x being set st x in ComplexBoundedFunctions X holds
NORM2 . x = upper_bound (PreNorms (modetrans (x,X))) ) implies NORM1 = NORM2 )
assume that
A1: for x being set st x in ComplexBoundedFunctions X holds
NORM1 . x = upper_bound (PreNorms (modetrans (x,X))) and
A2: for x being set st x in ComplexBoundedFunctions X holds
NORM2 . x = upper_bound (PreNorms (modetrans (x,X))) ; :: thesis: NORM1 = NORM2
A3: ( dom NORM1 = ComplexBoundedFunctions X & dom NORM2 = ComplexBoundedFunctions X ) by FUNCT_2:def 1;
for z being set st z in ComplexBoundedFunctions X holds
NORM1 . z = NORM2 . z

proof

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

end;

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