deffunc H₁( set ) -> Element of REAL = (Sum ((seq_id $1) rto_power p)) to_power (1 / p);
A1: for z being set st z in the_set_of_RealSequences_l^ p holds
H₁(z) in REAL ;
ex f being Function of (the_set_of_RealSequences_l^ p),REAL st
for x being set st x in the_set_of_RealSequences_l^ p holds
f . x = H₁(x) from FUNCT_2:sch 2(A1);
hence ex b₁ being Function of (the_set_of_RealSequences_l^ p),REAL st
for x being set st x in the_set_of_RealSequences_l^ p holds
b₁ . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p) ; :: thesis: verum