deffunc H₁( set ) -> object = |.(x . $1).| to_power p;
ex q1 being Real_Sequence st
for n being Nat holds q1 . n = H₁(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