defpred S_{1}[ object , object ] means ex n being Nat st

( n = $1 & $2 = F_{1}(n) );

A3: dom f = NAT and

A4: for x being object st x in NAT holds

S_{1}[x,f . x]
from CLASSES1:sch 1(A1);

take seq = f; :: thesis: for n being Nat holds seq . n = F_{1}(n)

let n be Nat; :: thesis: seq . n = F_{1}(n)

n in NAT by ORDINAL1:def 12;

then ex k being Nat st

( k = n & seq . n = F_{1}(k) )
by A4;

hence seq . n = F_{1}(n)
; :: thesis: verum

( n = $1 & $2 = F

A1: now :: thesis: for x being object st x in NAT holds

ex y being object st S_{1}[x,y]

consider f being Function such that ex y being object st S

let x be object ; :: thesis: ( x in NAT implies ex y being object st S_{1}[x,y] )

assume x in NAT ; :: thesis: ex y being object st S_{1}[x,y]

then consider n being Nat such that

A2: n = x ;

reconsider r2 = F_{1}(n) as object ;

take y = r2; :: thesis: S_{1}[x,y]

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

end;assume x in NAT ; :: thesis: ex y being object st S

then consider n being Nat such that

A2: n = x ;

reconsider r2 = F

take y = r2; :: thesis: S

thus S

A3: dom f = NAT and

A4: for x being object st x in NAT holds

S

now :: thesis: for x being object st x in NAT holds

f . x is real

then reconsider f = f as Real_Sequence by A3, Th1;f . x is real

let x be object ; :: thesis: ( x in NAT implies f . x is real )

assume x in NAT ; :: thesis: f . x is real

then ex n being Nat st

( n = x & f . x = F_{1}(n) )
by A4;

hence f . x is real ; :: thesis: verum

end;assume x in NAT ; :: thesis: f . x is real

then ex n being Nat st

( n = x & f . x = F

hence f . x is real ; :: thesis: verum

take seq = f; :: thesis: for n being Nat holds seq . n = F

let n be Nat; :: thesis: seq . n = F

n in NAT by ORDINAL1:def 12;

then ex k being Nat st

( k = n & seq . n = F

hence seq . n = F