reconsider a = a as Real by XREAL_0:def 1;
deffunc H₁( Element of NAT ) -> Element of REAL = a |^ $1;
ex f being Real_Sequence st
for m being Element of NAT holds f . m = H₁(m) from FUNCT_2:sch 4();
hence ex b₁ being Real_Sequence st
for m being Element of NAT holds b₁ . m = a |^ m ; :: thesis: verum