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

proof

let i be object ; :: thesis: ( i in NAT implies ex j being object st S₁[i,j] )
assume i in NAT ; :: thesis: ex j being object 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
A2: for i being object st i in NAT holds
S₁[i,f . i] from PBOOLE:sch 3(A1);
take f ; :: thesis: for n being Nat holds f . n = s . (n + k)
let n be Nat; :: thesis: f . n = s . (n + k)
S₁[n,f . n] by A2, ORDINAL1:def 12;
hence f . n = s . (n + k) ; :: thesis: verum