let k be Element of NAT ; :: thesis: ex seq being sequence of F₁() st
for n being Element of NAT holds
( ( n <= k implies seq . n = F₂(k,n) ) & ( n > k implies seq . n = 0. F₁() ) )
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. F₁() ) );

A1: now

let x be set ; :: thesis: ( x in NAT implies ex y being set st S₁[x,y] )
assume x in NAT ; :: thesis: ex y being set st S₁[x,y]
then consider n being Element of NAT such that
A2: n = x ;
reconsider chk = CHK n,k as Element of REAL by XREAL_0:def 1;

A3: now

assume n > k ; :: thesis: chk * F₂(k,n) = 0. F₁()
hence chk * F₂(k,n) = 0 * F₂(k,n) by SIN_COS:def 2
.= 0. F₁() by RLVECT_1:23 ;
:: thesis: verum

end;

reconsider y = chk * F₂(k,n) as set ;
take y = y; :: thesis: S₁[x,y]

now

assume n <= k ; :: thesis: chk * F₂(k,n) = F₂(k,n)
hence chk * F₂(k,n) = 1 * F₂(k,n) by SIN_COS:def 2
.= F₂(k,n) by RLVECT_1:def 11 ;
:: thesis: verum

end;

hence S₁[x,y] by A2, A3; :: thesis: verum

end;

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

now

let x be set ; :: thesis: ( x in NAT implies f . x in the carrier of F₁() )
assume x in NAT ; :: thesis: f . x in the carrier of F₁()
then ex n being Element of NAT st
( n = x & ( n <= k implies f . x = F₂(k,n) ) & ( n > k implies f . x = 0. F₁() ) ) by A5;
hence f . x in the carrier of F₁() ; :: thesis: verum

end;

then reconsider f = f as sequence of F₁() by A4, FUNCT_2:5;
take seq = f; :: thesis: for n being Element of NAT holds
( ( n <= k implies seq . n = F₂(k,n) ) & ( n > k implies seq . n = 0. F₁() ) )
let n be Element of NAT ; :: thesis: ( ( n <= k implies seq . n = F₂(k,n) ) & ( n > k implies seq . n = 0. F₁() ) )
ex l being Element of NAT st
( l = n & ( l <= k implies seq . n = F₂(k,l) ) & ( l > k implies seq . n = 0. F₁() ) ) by A5;
hence ( ( n <= k implies seq . n = F₂(k,n) ) & ( n > k implies seq . n = 0. F₁() ) ) ; :: thesis: verum