reconsider a = a as Real ;

deffunc H_{1}( 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_{1}(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_{1}(m)
by A1;

hence f . m = a |^ m ; :: thesis: verum

deffunc H

consider f being Real_Sequence such that

A1: for m being Element of NAT holds f . m = H

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

hence f . m = a |^ m ; :: thesis: verum