defpred S1[ 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 S1[x,y]
proof
let x be object ; :: thesis: ( x in j -' i implies ex y being object st S1[x,y] )
assume A2: x in j -' i ; :: thesis: ex y being object st S1[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: S1[x,y]
thus S1[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
S1[k,f . k] from reconsider f = f as ManySortedSet of j -' i by ;
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