deffunc H_{1}( set ) -> object = |.(x . $1).| to_power p;

ex q1 being Real_Sequence st

for n being Nat holds q1 . n = H_{1}(n)
from SEQ_1:sch 1();

then consider q1 being Real_Sequence such that

A1: for n being Nat holds q1 . n = |.(x . n).| to_power p ;

take q1 ; :: thesis: for n being Nat holds q1 . n = |.(x . n).| to_power p

thus for n being Nat holds q1 . n = |.(x . n).| to_power p by A1; :: thesis: verum

ex q1 being Real_Sequence st

for n being Nat holds q1 . n = H

then consider q1 being Real_Sequence such that

A1: for n being Nat holds q1 . n = |.(x . n).| to_power p ;

take q1 ; :: thesis: for n being Nat holds q1 . n = |.(x . n).| to_power p

thus for n being Nat holds q1 . n = |.(x . n).| to_power p by A1; :: thesis: verum