let k be Nat; :: thesis: ex seq being Complex_Sequence st
for n being Nat holds
( ( n <= k implies seq . n = F₁(k,n) ) & ( n > k implies seq . n = 0 ) )
defpred S₁[ object , object ] means ex n being Nat st
( n = $1 & ( n <= k implies $2 = F₁(k,n) ) & ( n > k implies $2 = 0c ) );

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 Nat such that
A2: n = x ;

A3: now :: thesis: ( n <= k implies (CHK (n,k)) * F₁(k,n) = F₁(k,n) )

assume n <= k ; :: thesis: (CHK (n,k)) * F₁(k,n) = F₁(k,n)
hence (CHK (n,k)) * F₁(k,n) = 1 * F₁(k,n) by Def1
.= F₁(k,n) ;
:: thesis: verum

end;

A4: now :: thesis: ( n > k implies (CHK (n,k)) * F₁(k,n) = 0 )

assume n > k ; :: thesis: (CHK (n,k)) * F₁(k,n) = 0
hence (CHK (n,k)) * F₁(k,n) = 0 * F₁(k,n) by Def1
.= 0 ;
:: thesis: verum

end;

reconsider y = (CHK (n,k)) * F₁(k,n) as object ;
take y = y; :: thesis: S₁[x,y]
thus S₁[x,y] by A2, A3, A4; :: thesis: verum

end;

consider f being Function such that
A5: dom f = NAT and
A6: 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 Nat st
( n = x & ( n <= k implies f . x = F₁(k,n) ) & ( n > k implies f . x = 0c ) ) by A6;
hence f . x is Element of COMPLEX by XCMPLX_0:def 2; :: thesis: verum

end;

then reconsider f = f as Complex_Sequence by A5, COMSEQ_1:1;
take seq = f; :: thesis: for n being Nat holds
( ( n <= k implies seq . n = F₁(k,n) ) & ( n > k implies seq . n = 0 ) )
let n be Nat; :: thesis: ( ( n <= k implies seq . n = F₁(k,n) ) & ( n > k implies seq . n = 0 ) )
n in NAT by ORDINAL1:def 12;
then S₁[n,f . n] by A6;
then ex l being Nat st
( l = n & ( l <= k implies seq . n = F₁(k,l) ) & ( l > k implies seq . n = 0c ) ) ;
hence ( ( n <= k implies seq . n = F₁(k,n) ) & ( n > k implies seq . n = 0 ) ) ; :: thesis: verum