deffunc H₁( object ) -> object = Sum (abs (seq_id $1));
A1: for z being object st z in the_set_of_l1RealSequences holds
H₁(z) in REAL by XREAL_0:def 1;
ex f being Function of the_set_of_l1RealSequences,REAL st
for x being object st x in the_set_of_l1RealSequences holds
f . x = H₁(x) from FUNCT_2:sch 2(A1);
hence ex b₁ being Function of the_set_of_l1RealSequences,REAL st
for x being object st x in the_set_of_l1RealSequences holds
b₁ . x = Sum (abs (seq_id x)) ; :: thesis: verum