defpred S₁[ set , set ] means ex k1 being Element of NAT st
( k1 = $1 & $2 = b . (i + k1) );

now :: thesis: for x being set st x in j -' i holds
ex y being set st S₁[x,y]

let x be set ; :: thesis: ( x in j -' i implies ex y being set st S₁[x,y] )
assume A1: x in j -' i ; :: thesis: ex y being set st S₁[x,y]
j -' i = { k where k is Element of NAT : k < j -' i } by AXIOMS:4;
then ex k being Element of NAT st
( x = k & k < j -' i ) by A1;
then reconsider x9 = x as Element of NAT ;
consider y being set such that
A2: y = b . (i + x9) ;
take y = y; :: thesis: S₁[x,y]
thus S₁[x,y] by A2; :: thesis: verum

end;

then A3: for x being set st x in j -' i holds
ex y being set st S₁[x,y] ;
consider f being Function such that
A4: dom f = j -' i and
A5: for k being set st k in j -' i holds
S₁[k,f . k] from CLASSES1:sch 1(A3);
reconsider f = f as ManySortedSet of j -' i by A4, PARTFUN1:def 2, RELAT_1:def 18;
take f ; :: thesis: for k being Element of NAT st k in j -' i holds
f . k = b . (i + k)
let k be Element of NAT ; :: thesis: ( k in j -' i implies f . k = b . (i + k) )
assume k in j -' i ; :: thesis: f . k = b . (i + k)
then ex k9 being Element of NAT st
( k9 = k & f . k = b . (i + k9) ) by A5;
hence f . k = b . (i + k) ; :: thesis: verum