deffunc H₁( set ) -> Element of REAL = (abs (x . $1)) to_power p;
ex q1 being Real_Sequence st
for n being Element of NAT holds q1 . n = H₁(n) from SEQ_1:sch 1();
then consider q1 being Real_Sequence such that
A1: for n being Element of NAT holds q1 . n = (abs (x . n)) to_power p ;
take q1 ; :: thesis: for n being Element of NAT holds q1 . n = (abs (x . n)) to_power p
thus for n being Element of NAT holds q1 . n = (abs (x . n)) to_power p by A1; :: thesis: verum