defpred S₁[ set , set ] means ex n being Element of NAT st
( n = $1 & $2 = s . (n + k) );
A0: for i being set st i in NAT holds
ex j being set st S₁[i,j]

proof

let i be set ; :: thesis: ( i in NAT implies ex j being set st S₁[i,j] )
assume i in NAT ; :: thesis: ex j being set st S₁[i,j]
then reconsider n = i as Element of NAT ;
take j = s . (n + k); :: thesis: S₁[i,j]
thus S₁[i,j] ; :: thesis: verum

end;

consider f being ManySortedSet of NAT such that
A1: for i being set st i in NAT holds
S₁[i,f . i] from PBOOLE:sch 3(A0);
take f ; :: thesis: for n being Nat holds f . n = s . (n + k)
let n be Nat; :: thesis: f . n = s . (n + k)
n in NAT by ORDINAL1:def 12;
then S₁[n,f . n] by A1;
hence f . n = s . (n + k) ; :: thesis: verum