hereby :: thesis: ( not len p > 0 implies ex b1 being Polynomial of L st b1 = 0_. L )
r in Roots p by ;
then A2: len p <> 1 by Th43;
deffunc H1( Nat) -> Element of the carrier of L = eval ((poly_shift (p,(\$1 + 1))),r);
set lq = (len p) -' 1;
consider q being sequence of L such that
A3: for k being Element of NAT holds q . k = H1(k) from reconsider q = q as sequence of L ;
assume A4: len p > 0 ; :: thesis: ex q being AlgSequence of L st
( (len q) + 1 = len p & ( for k being Nat holds q . k = H1(k) ) )

then consider p1 being Nat such that
A5: len p = p1 + 1 by NAT_1:6;
A6: (len p) -' 1 = p1 by ;
then A7: (len p) -' 1 < len p by ;
len p >= 0 + 1 by ;
then consider lq1 being Nat such that
A8: (len p) -' 1 = lq1 + 1 by ;
A9: now :: thesis: for i being Nat st i >= (len p) -' 1 holds
q . i = 0. L
let i be Nat; :: thesis: ( i >= (len p) -' 1 implies q . i = 0. L )
assume i >= (len p) -' 1 ; :: thesis: q . i = 0. L
then i >= p1 by ;
then A10: i + 1 >= len p by ;
i in NAT by ORDINAL1:def 12;
hence q . i = eval ((poly_shift (p,(i + 1))),r) by A3
.= eval ((0_. L),r) by
.= 0. L by POLYNOM4:17 ;
:: thesis: verum
end;
reconsider lq1 = lq1 as Element of NAT by ORDINAL1:def 12;
q . lq1 = eval ((poly_shift (p,(lq1 + 1))),r) by A3
.= (r * (eval ((poly_shift (p,(len p))),r))) + (p . ((len p) -' 1)) by A5, A6, A8, A7, Th42
.= (r * (eval ((0_. L),r))) + (p . ((len p) -' 1)) by Th40
.= (r * (0. L)) + (p . ((len p) -' 1)) by POLYNOM4:17
.= (0. L) + (p . ((len p) -' 1))
.= p . ((len p) -' 1) by RLVECT_1:4 ;
then A11: q . lq1 <> 0. L by ;
reconsider q = q as AlgSequence of L by ;
A12: lq1 = ((len p) -' 1) -' 1 by ;
A13: now :: thesis: for m being Nat st m is_at_least_length_of q holds
not (len p) -' 1 > m
let m be Nat; :: thesis: ( m is_at_least_length_of q implies not (len p) -' 1 > m )
assume A14: m is_at_least_length_of q ; :: thesis: not (len p) -' 1 > m
assume A15: (len p) -' 1 > m ; :: thesis: contradiction
then consider lq1 being Nat such that
A16: (len p) -' 1 = lq1 + 1 by NAT_1:6;
lq1 >= m by ;
then ((len p) -' 1) -' 1 >= m by ;
hence contradiction by A12, A11, A14, ALGSEQ_1:def 2; :: thesis: verum
end;
take q = q; :: thesis: ( (len q) + 1 = len p & ( for k being Nat holds q . k = H1(k) ) )
(len p) -' 1 is_at_least_length_of q by ;
hence (len q) + 1 = ((p1 + 1) -' 1) + 1 by
.= len p by ;
:: thesis: for k being Nat holds q . k = H1(k)
let k be Nat; :: thesis: q . k = H1(k)
k in NAT by ORDINAL1:def 12;
hence q . k = H1(k) by A3; :: thesis: verum
end;
thus ( not len p > 0 implies ex b1 being Polynomial of L st b1 = 0_. L ) ; :: thesis: verum