deffunc H_{1}( object ) -> object = (Sum ((seq_id $1) rto_power p)) to_power (1 / p);

A1: for z being object st z in the_set_of_RealSequences_l^ p holds

H_{1}(z) in REAL
by XREAL_0:def 1;

ex f being Function of (the_set_of_RealSequences_l^ p),REAL st

for x being object st x in the_set_of_RealSequences_l^ p holds

f . x = H_{1}(x)
from FUNCT_2:sch 2(A1);

hence ex b_{1} being Function of (the_set_of_RealSequences_l^ p),REAL st

for x being object st x in the_set_of_RealSequences_l^ p holds

b_{1} . x = (Sum ((seq_id x) rto_power p)) to_power (1 / p)
; :: thesis: verum

A1: for z being object st z in the_set_of_RealSequences_l^ p holds

H

ex f being Function of (the_set_of_RealSequences_l^ p),REAL st

for x being object st x in the_set_of_RealSequences_l^ p holds

f . x = H

hence ex b

for x being object st x in the_set_of_RealSequences_l^ p holds

b