deffunc H₁( set ) -> Element of S = pai . ((k_nat $1) + k);
A1: for x being set st x in NAT holds
H₁(x) in S ;
consider IT being Function of NAT,S such that
A2: for n being set st n in NAT holds
IT . n = H₁(n) from FUNCT_2:sch 2(A1);
A3: for n being Element of NAT holds IT . n = pai . (n + k)

proof

let n be Element of NAT ; :: thesis: IT . n = pai . (n + k)
H₁(n) = pai . (n + k) by Def2;
hence IT . n = pai . (n + k) by A2; :: thesis: verum

end;

for n being Element of NAT holds [(IT . n),(IT . (n + 1))] in R

proof

let n be Element of NAT ; :: thesis: [(IT . n),(IT . (n + 1))] in R
set n1 = n + 1;
set n2 = n + k;
A4: IT . (n + 1) = pai . ((n + 1) + k) by A3
.= pai . ((n + k) + 1) ;
IT . n = pai . (n + k) by A3;
hence [(IT . n),(IT . (n + 1))] in R by A4, Def41; :: thesis: verum

end;

then reconsider IT = IT as inf_path of R by Def41;
take IT ; :: thesis: for n being Element of NAT holds IT . n = pai . (n + k)
thus for n being Element of NAT holds IT . n = pai . (n + k) by A3; :: thesis: verum