defpred S₁[ object , object ] means ex n being Element of NAT st
( n = $1 & $2 = F₁(n) );

A1: now :: thesis: for x being object st x in NAT holds
ex y being object st S₁[x,y]

let x be object ; :: thesis: ( x in NAT implies ex y being object st S₁[x,y] )
assume x in NAT ; :: thesis: ex y being object st S₁[x,y]
then consider n being Element of NAT such that
A2: n = x ;
reconsider r2 = F₁(n) as object ;
take y = r2; :: thesis: S₁[x,y]
thus S₁[x,y] by A2; :: thesis: verum

end;

consider f being Function such that
A3: dom f = NAT and
A4: for x being object st x in NAT holds
S₁[x,f . x] from CLASSES1:sch 1(A1);

now :: thesis: for x being set st x in NAT holds
f . x is Element of COMPLEX

let x be set ; :: thesis: ( x in NAT implies f . x is Element of COMPLEX )
assume x in NAT ; :: thesis: f . x is Element of COMPLEX
then ex n being Element of NAT st
( n = x & f . x = F₁(n) ) by A4;
hence f . x is Element of COMPLEX by XCMPLX_0:def 2; :: thesis: verum

end;

then reconsider f = f as Complex_Sequence by A3, Th1;
take seq = f; :: thesis: for n being Nat holds seq . n = F₁(n)
let n be Nat; :: thesis: seq . n = F₁(n)
n in NAT by ORDINAL1:def 12;
then ex k being Element of NAT st
( k = n & seq . n = F₁(k) ) by A4;
hence seq . n = F₁(n) ; :: thesis: verum