reconsider k9 = k as Element of NAT by ORDINAL1:def 12;
deffunc H₁( Element of NAT ) -> Element of omega = $1 |^ k9;
consider f being sequence of NAT such that
A1: for n being Element of NAT holds f . n = H₁(n) from FUNCT_2:sch 4();
take f ; :: thesis: for n being Nat holds f . n = n |^ k
for n being Nat holds f . n = n |^ k

proof

let n be Nat; :: thesis: f . n = n |^ k
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
f . n9 = H₁(n9) by A1;
hence f . n = n |^ k ; :: thesis: verum

end;

hence for n being Nat holds f . n = n |^ k ; :: thesis: verum