let k be Nat; ex rseq being Real_Sequence st
for n being Nat holds
( ( n <= k implies rseq . n = F1(k,n) ) & ( n > k implies rseq . n = 0 ) )
defpred S1[ object , object ] means ex n being Nat st
( n = $1 & ( n <= k implies $2 = F1(k,n) ) & ( n > k implies $2 = 0 ) );
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
;
A3:
now ( n <= k implies (CHK (n,k)) * F1(k,n) = F1(k,n) )assume
n <= k
;
(CHK (n,k)) * F1(k,n) = F1(k,n)hence (CHK (n,k)) * F1(
k,
n) =
1
* F1(
k,
n)
by Def1
.=
F1(
k,
n)
;
verum end; A4:
now ( n > k implies (CHK (n,k)) * F1(k,n) = 0 )assume
n > k
;
(CHK (n,k)) * F1(k,n) = 0 hence (CHK (n,k)) * F1(
k,
n) =
0 * F1(
k,
n)
by Def1
.=
0
;
verum end; reconsider y =
(CHK (n,k)) * F1(
k,
n) as
object ;
take y =
y;
S1[x,y]thus
S1[
x,
y]
by A2, A3, A4;
verum end;
consider f being Function such that
A5:
dom f = NAT
and
A6:
for x being object st x in NAT holds
S1[x,f . x]
from CLASSES1:sch 1(A1);
then reconsider f = f as Real_Sequence by A5, SEQ_1:1;
take rseq = f; for n being Nat holds
( ( n <= k implies rseq . n = F1(k,n) ) & ( n > k implies rseq . n = 0 ) )
let n be Nat; ( ( n <= k implies rseq . n = F1(k,n) ) & ( n > k implies rseq . n = 0 ) )
n in NAT
by ORDINAL1:def 12;
then
ex l being Nat st
( l = n & ( l <= k implies rseq . n = F1(k,l) ) & ( l > k implies rseq . n = 0 ) )
by A6;
hence
( ( n <= k implies rseq . n = F1(k,n) ) & ( n > k implies rseq . n = 0 ) )
; verum