deffunc H₁( set ) -> Element of REAL = upper_bound (rng |.(seq_id $1).|);
A1: for z being set st z in the_set_of_BoundedComplexSequences holds
H₁(z) in REAL ;
ex f being Function of the_set_of_BoundedComplexSequences ,REAL st
for x being set st x in the_set_of_BoundedComplexSequences holds
f . x = H₁(x) from FUNCT_2:sch 2(A1);
hence ex NORM being Function of the_set_of_BoundedComplexSequences ,REAL st
for x being set st x in the_set_of_BoundedComplexSequences holds
NORM . x = sup (rng |.(seq_id x).|) ; :: thesis: verum