defpred S₁[ object , object ] means ex k being Element of NAT st
( k = $1 & ( ( k < m & $2 = eval (p,(x |^ k)) ) or ( m <= k & $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 < m or u9 >= m ) ;

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

take eval (p,(x |^ u9)) ; :: thesis: ( eval (p,(x |^ u9)) in the carrier of L & S₁[u, eval (p,(x |^ u9))] )
thus ( eval (p,(x |^ u9)) in the carrier of L & S₁[u, eval (p,(x |^ u9))] ) by A2; :: thesis: verum

end;

suppose A3: u9 >= m ; :: 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 ;
ex n being Nat st
for i being Nat st i >= n holds
f . i = 0. L

proof

reconsider m = m as Element of NAT by ORDINAL1:def 12;
take m ; :: thesis: for i being Nat st i >= m holds
f . i = 0. L

now :: thesis: for i being Nat st i >= m holds
f . i = 0. L

let i be Nat; :: thesis: ( i >= m implies f . i = 0. L )
i in NAT by ORDINAL1:def 12;
then A5: ex k being Element of NAT st
( k = i & ( ( k < m & f . i = eval (p,(x |^ k)) ) or ( m <= k & f . i = 0. L ) ) ) by A4;
assume i >= m ; :: thesis: f . i = 0. L
hence f . i = 0. L by A5; :: thesis: verum

end;

hence for i being Nat st i >= m holds
f . i = 0. L ; :: thesis: verum

end;

then reconsider q = f as AlgSequence of L by ALGSEQ_1:def 1;

A6: now :: thesis: for i being Nat st i >= m holds
q . i = 0. L

let i be Nat; :: thesis: ( i >= m implies q . i = 0. L )
i in NAT by ORDINAL1:def 12;
then A7: ex k being Element of NAT st
( k = i & ( ( k < m & q . i = eval (p,(x |^ k)) ) or ( m <= k & q . i = 0. L ) ) ) by A4;
assume i >= m ; :: thesis: q . i = 0. L
hence q . i = 0. L by A7; :: thesis: verum

end;

take q ; :: thesis: ( ( for i being Nat st i < m holds
q . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds
q . i = 0. L ) )

now :: thesis: for i being Nat st i < m holds
q . i = eval (p,(x |^ i))

let i be Nat; :: thesis: ( i < m implies q . i = eval (p,(x |^ i)) )
i in NAT by ORDINAL1:def 12;
then A8: ex k being Element of NAT st
( k = i & ( ( k < m & q . i = eval (p,(x |^ k)) ) or ( m <= k & q . i = 0. L ) ) ) by A4;
assume i < m ; :: thesis: q . i = eval (p,(x |^ i))
hence q . i = eval (p,(x |^ i)) by A8; :: thesis: verum

end;

hence ( ( for i being Nat st i < m holds
q . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds
q . i = 0. L ) ) by A6; :: thesis: verum