deffunc H₁( Element of NAT ) -> Element of NAT = sigma (k,$1);
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 = sigma (k,n)
let n be Nat; :: thesis: f . n = sigma (k,n)
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
thus f . n = f . n9
.= sigma (k,n) by A1 ; :: thesis: verum