deffunc H_{1}( 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_{1}(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

consider f being sequence of NAT such that

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

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