reconsider k' = k as Element of NAT by ORDINAL1:def 13;
deffunc H₁( Element of NAT ) -> Element of NAT = $1 |^ k';
consider f being Function of NAT , 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 natural number holds f . n = n |^ k
for n being natural number holds f . n = n |^ k

proof

let n be natural number ; :: thesis: f . n = n |^ k
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
f . n' = H₁(n') by A1;
hence f . n = n |^ k ; :: thesis: verum

end;

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