reconsider a = a as Real ;
deffunc H₁( Nat) -> Element of REAL = In ((a |^ $1),REAL);
consider f being Real_Sequence such that
A1: for m being Element of NAT holds f . m = H₁(m) from FUNCT_2:sch 4();
take f ; :: thesis: for m being Nat holds f . m = a |^ m
let m be Nat; :: thesis: f . m = a |^ m
reconsider m = m as Element of NAT by ORDINAL1:def 12;
f . m = H₁(m) by A1;
hence f . m = a |^ m ; :: thesis: verum