deffunc H1( set ) -> Element of REAL = Sum (abs (seq_id $1));
A1:
for z being set st z in the_set_of_l1RealSequences holds
H1(z) in REAL
;
ex f being Function of the_set_of_l1RealSequences,REAL st
for x being set st x in the_set_of_l1RealSequences holds
f . x = H1(x)
from FUNCT_2:sch 2(A1);
hence
ex NORM being Function of the_set_of_l1RealSequences,REAL st
for x being set st x in the_set_of_l1RealSequences holds
NORM . x = Sum (abs (seq_id x))
; verum