defpred S₁[ object , object ] 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 object st x in NAT holds
ex y being object st
( y in the carrier of L & S₁[x,y] )

proof

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

per cases ( u9 < k or u9 >= k ) ;

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

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

end;

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

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

end;

end;

end;

consider f being sequence of the carrier of L such that
A4: for x being object 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 )
i in NAT by ORDINAL1:def 12;
then A6: ex n being Element of NAT st
( n = i & ( n < k implies f . i = (power L) . (z,((k - n) - 1)) ) & ( n >= k implies f . i = 0. L ) ) by A4;
assume i >= k ; :: thesis: f . i = 0. L
hence f . i = 0. L by A6; :: thesis: verum

end;

then reconsider p = f as AlgSequence of L by ALGSEQ_1:def 1;
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 :: thesis: for i being Nat st i < k holds
p . i = (power L) . (z,((k - i) - 1))

let i be Nat; :: thesis: ( i < k implies p . i = (power L) . (z,((k - i) - 1)) )
i in NAT by ORDINAL1:def 12;
then A7: ex n being Element of NAT st
( n = i & ( n < k implies f . i = (power L) . (z,((k - n) - 1)) ) & ( n >= k implies f . i = 0. L ) ) by A4;
assume i < k ; :: thesis: p . i = (power L) . (z,((k - i) - 1))
hence p . i = (power L) . (z,((k - i) - 1)) by A7; :: 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