deffunc H1( object ) -> Element of S = pai . ((k_nat $1) + k);
A1: for x being object st x in NAT holds
H1(x) in S ;
consider IT being sequence of S such that
A2: for n being object st n in NAT holds
IT . n = H1(n) from FUNCT_2:sch 2(A1);
 A3: for n being Nat holds IT . n = pai . (n + k)
proof
let n be Nat; :: thesis: IT . n = pai . (n + k)
A4: n in NAT by ORDINAL1:def 12;
then H1(n) = pai . (n + k) by Def2;
hence IT . n = pai . (n + k) by A2, A4; :: thesis: verum
end;
for n being Nat holds [(IT . n),(IT . (n + 1))] in R
proof
let n be Nat; :: thesis: [(IT . n),(IT . (n + 1))] in R
set n1 = n + 1;
set n2 = n + k;
A5: 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 A5, Def39; :: thesis: verum
end;
then reconsider IT = IT as inf_path of R by Def39;
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