defpred S_{1}[ 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_{1}[x,y] )

A4: for x being object st x in NAT holds

S_{1}[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

q . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds

q . i = 0. L ) )

q . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds

q . i = 0. L ) ) by A6; :: thesis: verum

( 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

proof

consider f being sequence of the carrier of L such that
let u be object ; :: thesis: ( u in NAT implies ex y being object st

( y in the carrier of L & S_{1}[u,y] ) )

assume u in NAT ; :: thesis: ex y being object st

( y in the carrier of L & S_{1}[u,y] )

then reconsider u9 = u as Element of NAT ;

end;( y in the carrier of L & S

assume u in NAT ; :: thesis: ex y being object st

( y in the carrier of L & S

then reconsider u9 = u as Element of NAT ;

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

end;

suppose A2:
u9 < m
; :: thesis: ex y being object st

( y in the carrier of L & S_{1}[u,y] )

( y in the carrier of L & S

take
eval (p,(x |^ u9))
; :: thesis: ( eval (p,(x |^ u9)) in the carrier of L & S_{1}[u, eval (p,(x |^ u9))] )

thus ( eval (p,(x |^ u9)) in the carrier of L & S_{1}[u, eval (p,(x |^ u9))] )
by A2; :: thesis: verum

end;thus ( eval (p,(x |^ u9)) in the carrier of L & S

A4: for x being object st x in NAT holds

S

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

then reconsider q = f as AlgSequence of L by ALGSEQ_1:def 1;
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

f . i = 0. L ; :: thesis: verum

end;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

hence
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;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

f . i = 0. L ; :: thesis: verum

A6: now :: thesis: for i being Nat st i >= m holds

q . i = 0. L

take
q
; :: 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;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

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))

hence
( ( 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;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

q . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds

q . i = 0. L ) ) by A6; :: thesis: verum