let NORM1, NORM2 be Function of the_set_of_BoundedComplexSequences,REAL; :: thesis: ( ( for x being object st x in the_set_of_BoundedComplexSequences holds
NORM1 . x = upper_bound (rng |.().|) ) & ( for x being object st x in the_set_of_BoundedComplexSequences holds
NORM2 . x = upper_bound (rng |.().|) ) implies NORM1 = NORM2 )

assume that
A2: for x being object st x in the_set_of_BoundedComplexSequences holds
NORM1 . x = upper_bound (rng |.().|) and
A3: for x being object st x in the_set_of_BoundedComplexSequences holds
NORM2 . x = upper_bound (rng |.().|) ; :: thesis: NORM1 = NORM2
A4: for z being object st z in the_set_of_BoundedComplexSequences holds
NORM1 . z = NORM2 . z
proof
let z be object ; :: thesis: ( z in the_set_of_BoundedComplexSequences implies NORM1 . z = NORM2 . z )
assume A5: z in the_set_of_BoundedComplexSequences ; :: thesis: NORM1 . z = NORM2 . z
NORM1 . z = upper_bound (rng |.().|) by A2, A5;
hence NORM1 . z = NORM2 . z by A3, A5; :: thesis: verum
end;
( dom NORM1 = the_set_of_BoundedComplexSequences & dom NORM2 = the_set_of_BoundedComplexSequences ) by FUNCT_2:def 1;
hence NORM1 = NORM2 by ; :: thesis: verum