let k be Nat; :: thesis: 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 :: thesis: for x being object st x in NAT holds
ex y being object st S1[x,y]
let x be object ; :: thesis: ( x in NAT implies ex y being object st S1[x,y] )
assume x in NAT ; :: thesis: ex y being object st S1[x,y]
then consider n being Nat such that
A2: n = x ;
reconsider chk = CHK (n,k) as Element of REAL by XREAL_0:def 1;
A3: ( n > k implies chk * F2(k,n) = 0. F1() ) by RLVECT_1:10, SIN_COS:def 1;
reconsider y = chk * F2(k,n) as object ;
take y = y; :: thesis: S1[x,y]
now :: thesis: ( n <= k implies chk * F2(k,n) = F2(k,n) )
assume n <= k ; :: thesis: chk * F2(k,n) = F2(k,n)
hence chk * F2(k,n) = 1 * F2(k,n) by SIN_COS:def 1
.= F2(k,n) by RLVECT_1:def 8 ;
:: thesis: verum
end;
hence S1[x,y] by A2, A3; :: thesis: 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);
now :: thesis: for x being object st x in NAT holds
f . x in the carrier of F1()
let x be object ; :: thesis: ( x in NAT implies f . x in the carrier of F1() )
assume x in NAT ; :: thesis: f . x in the carrier of F1()
then ex n being Nat st
( n = x & ( n <= k implies f . x = F2(k,n) ) & ( n > k implies f . x = 0. F1() ) ) by A5;
hence f . x in the carrier of F1() ; :: thesis: verum
end;
then reconsider f = f as sequence of F1() by A4, FUNCT_2:3;
take seq = f; :: thesis: for n being Nat holds
( ( n <= k implies seq . n = F2(k,n) ) & ( n > k implies seq . n = 0. F1() ) )
let n be Nat; :: thesis: ( ( n <= k implies seq . n = F2(k,n) ) & ( n > k implies seq . n = 0. F1() ) )
A6: n in NAT by ORDINAL1:def 12;
ex l being Nat st
( l = n & ( l <= k implies seq . n = F2(k,l) ) & ( l > k implies seq . n = 0. F1() ) ) by A5, A6;
hence ( ( n <= k implies seq . n = F2(k,n) ) & ( n > k implies seq . n = 0. F1() ) ) ; :: thesis: verum