let k be Element of NAT ; :: thesis: ex rseq being Real_Sequence st
for n being Element of NAT holds
( ( n <= k implies rseq . n = F₁(k,n) ) & ( n > k implies rseq . n = 0 ) )
defpred S₁[ set , set ] means ex n being Element of NAT st
( n = $1 & ( n <= k implies $2 = F₁(k,n) ) & ( n > k implies $2 = 0 ) );

A1: now

let x be set ; :: thesis: ( x in NAT implies ex y being set st S₁[x,y] )
assume A2: x in NAT ; :: thesis: ex y being set st S₁[x,y]
consider n being Element of NAT such that
A3: n = x by A2;

A4: now

assume A5: n <= k ; :: thesis: (CHK n,k) * F₁(k,n) = F₁(k,n)
thus (CHK n,k) * F₁(k,n) = 1 * F₁(k,n) by A5, Def2
.= F₁(k,n) ; :: thesis: verum

end;

A6: now

assume A7: n > k ; :: thesis: (CHK n,k) * F₁(k,n) = 0
thus (CHK n,k) * F₁(k,n) = 0 * F₁(k,n) by A7, Def2
.= 0 ; :: thesis: verum

end;

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

end;

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

A10: now

let x be set ; :: thesis: ( x in NAT implies f . x is real )
assume A11: x in NAT ; :: thesis: f . x is real
A12: ex n being Element of NAT st
( n = x & ( n <= k implies f . x = F₁(k,n) ) & ( n > k implies f . x = 0 ) ) by A9, A11;
thus f . x is real by A12; :: thesis: verum

end;

reconsider f = f as Real_Sequence by A8, A10, SEQ_1:3;
take rseq = f; :: thesis: for n being Element of NAT holds
( ( n <= k implies rseq . n = F₁(k,n) ) & ( n > k implies rseq . n = 0 ) )
let n be Element of NAT ; :: thesis: ( ( n <= k implies rseq . n = F₁(k,n) ) & ( n > k implies rseq . n = 0 ) )
A13: ex l being Element of NAT st
( l = n & ( l <= k implies rseq . n = F₁(k,l) ) & ( l > k implies rseq . n = 0 ) ) by A9;
thus ( ( n <= k implies rseq . n = F₁(k,n) ) & ( n > k implies rseq . n = 0 ) ) by A13; :: thesis: verum