deffunc H₁( set ) -> Element of S = t . ((CastNat $1) + k);
A1: for x being set st x in NAT holds
H₁(x) in S ;
consider IT being sequence of S such that
A2: for n being set st n in NAT holds
IT . n = H₁(n) from FUNCT_2:sch 2(A1);
take IT ; :: thesis: for n being Nat holds IT . n = t . (n + k)
for n being Nat holds IT . n = t . (n + k)

proof

let n be Nat; :: thesis: IT . n = t . (n + k)
( H₁(n) = t . (n + k) & n in NAT ) by Def1, ORDINAL1:def 13;
hence IT . n = t . (n + k) by A2; :: thesis: verum

end;

hence for n being Nat holds IT . n = t . (n + k) ; :: thesis: verum