defpred S₁[ object , object ] means ex k1 being Element of NAT st
( k1 = $1 & $2 = b . (i + k1) );
A1: for x being object st x in j -' i holds
ex y being object st S₁[x,y]

proof

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

end;

consider f being Function such that
A4: dom f = j -' i and
A5: for k being object st k in j -' i holds
S₁[k,f . k] from CLASSES1:sch 1(A1);
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