defpred S₁[ set , set ] means ex n being Element of NAT st
( n = $1 & ( n < k implies $2 = (power L) . z,((k - n) - 1) ) & ( n >= k implies $2 = 0. L ) );
A1: for x being set st x in NAT holds
ex y being set st
( y in the carrier of L & S₁[x,y] )

proof

let u be set ; :: thesis: ( u in NAT implies ex y being set st
( y in the carrier of L & S₁[u,y] ) )
assume u in NAT ; :: thesis: ex y being set st
( y in the carrier of L & S₁[u,y] )
then reconsider u' = u as Element of NAT ;
thus ex y being set st
( y in the carrier of L & S₁[u,y] ) :: thesis: verum

proof

per cases ( u' < k or u' >= k ) ;

suppose A2: u' < k ; :: thesis: ex y being set st
( y in the carrier of L & S₁[u,y] )

take y = (power L) . z,((k - u') - 1); :: thesis: ( y in the carrier of L & S₁[u,y] )
reconsider ku = k - u' as Element of NAT by A2, INT_1:18;
k - k < ku by A2, XREAL_1:12;
then 0 + 1 < ku + 1 by XREAL_1:8;
then 1 <= k - u' by NAT_1:13;
then reconsider m = (k - u') - 1 as Element of NAT by INT_1:18;
(power L) . z,m in the carrier of L ;
hence ( y in the carrier of L & S₁[u,y] ) by A2; :: thesis: verum

end;

suppose A3: u' >= k ; :: thesis: ex y being set st
( y in the carrier of L & S₁[u,y] )

take y = 0. L; :: thesis: ( y in the carrier of L & S₁[u,y] )
thus ( y in the carrier of L & S₁[u,y] ) by A3; :: thesis: verum

end;

end;

end;

end;

consider f being Function of NAT ,the carrier of L such that
A4: for x being set st x in NAT holds
S₁[x,f . x] from FUNCT_2:sch 1(A1);
reconsider f = f as sequence of L ;
A5: for i being Nat st i >= k holds
f . i = 0. L

proof

let i be Nat; :: thesis: ( i >= k implies f . i = 0. L )
assume A6: i >= k ; :: thesis: f . i = 0. L
i in NAT by ORDINAL1:def 13;
then consider n being Element of NAT such that
A7: ( n = i & ( n < k implies f . i = (power L) . z,((k - n) - 1) ) & ( n >= k implies f . i = 0. L ) ) by A4;
thus f . i = 0. L by A6, A7; :: thesis: verum

end;

then reconsider p = f as AlgSequence of L by ALGSEQ_1:def 2;
take p ; :: thesis: ( ( for i being Nat st i < k holds
p . i = (power L) . z,((k - i) - 1) ) & ( for i being Nat st i >= k holds
p . i = 0. L ) )

now

let i be Nat; :: thesis: ( i < k implies p . i = (power L) . z,((k - i) - 1) )
assume A8: i < k ; :: thesis: p . i = (power L) . z,((k - i) - 1)
i in NAT by ORDINAL1:def 13;
then consider n being Element of NAT such that
A9: ( n = i & ( n < k implies f . i = (power L) . z,((k - n) - 1) ) & ( n >= k implies f . i = 0. L ) ) by A4;
thus p . i = (power L) . z,((k - i) - 1) by A8, A9; :: thesis: verum

end;

hence ( ( for i being Nat st i < k holds
p . i = (power L) . z,((k - i) - 1) ) & ( for i being Nat st i >= k holds
p . i = 0. L ) ) by A5; :: thesis: verum