defpred S_{1}[ 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_{1}[x,y]

A4: dom f = j -' i and

A5: for k being object st k in j -' i holds

S_{1}[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

( k1 = $1 & $2 = b . (i + k1) );

A1: for x being object st x in j -' i holds

ex y being object st S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in j -' i implies ex y being object st S_{1}[x,y] )

assume A2: x in j -' i ; :: thesis: ex y being object st S_{1}[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_{1}[x,y]

thus S_{1}[x,y]
by A3; :: thesis: verum

end;assume A2: x in j -' i ; :: thesis: ex y being object st S

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

thus S

A4: dom f = j -' i and

A5: for k being object st k in j -' i holds

S

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