let k be Nat; ex seq being sequence of F1() st
for n being Nat holds
( ( n <= k implies seq . n = F2(k,n) ) & ( n > k implies seq . n = 0. F1() ) )
defpred S1[ object , object ] means ex n being Nat st
( n = $1 & ( n <= k implies $2 = F2(k,n) ) & ( n > k implies $2 = 0. F1() ) );
A1:
now for x being object st x in NAT holds
ex y being object st S1[x,y]let x be
object ;
( x in NAT implies ex y being object st S1[x,y] )assume
x in NAT
;
ex y being object st S1[x,y]then consider n being
Nat such that A2:
n = x
;
reconsider y =
(CHK (n,k)) * F2(
k,
n) as
object ;
A3:
(
n > k implies
(CHK (n,k)) * F2(
k,
n)
= 0. F1() )
by CLVECT_1:1, SIN_COS:def 1;
take y =
y;
S1[x,y]now ( n <= k implies (CHK (n,k)) * F2(k,n) = F2(k,n) )end; hence
S1[
x,
y]
by A2, A3;
verum end;
consider f being Function such that
A4:
dom f = NAT
and
A5:
for x being object st x in NAT holds
S1[x,f . x]
from CLASSES1:sch 1(A1);
then reconsider f = f as sequence of F1() by A4, FUNCT_2:3;
take seq = f; for n being Nat holds
( ( n <= k implies seq . n = F2(k,n) ) & ( n > k implies seq . n = 0. F1() ) )
let n be Nat; ( ( n <= k implies seq . n = F2(k,n) ) & ( n > k implies seq . n = 0. F1() ) )
n in NAT
by ORDINAL1:def 12;
then
ex l being Nat st
( l = n & ( l <= k implies seq . n = F2(k,l) ) & ( l > k implies seq . n = 0. F1() ) )
by A5;
hence
( ( n <= k implies seq . n = F2(k,n) ) & ( n > k implies seq . n = 0. F1() ) )
; verum