hereby :: thesis: ( not len p > 0 implies ex b₁ being Polynomial of L st b₁ = 0_. L )

r in Roots p by A1, POLYNOM5:def 10;
then A2: len p <> 1 by Th43;
deffunc H₁( 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 = H₁(k) from FUNCT_2:sch 4();
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 = H₁(k) ) )
then consider p1 being Nat such that
A5: len p = p1 + 1 by NAT_1:6;
A6: (len p) -' 1 = p1 by A5, NAT_D:34;
then A7: (len p) -' 1 < len p by A5, NAT_1:13;
len p >= 0 + 1 by A4, NAT_1:13;
then consider lq1 being Nat such that
A8: (len p) -' 1 = lq1 + 1 by A5, A6, A2, NAT_1:6;

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 A5, NAT_D:34;
then A10: i + 1 >= len p by A5, XREAL_1:6;
i in NAT by ORDINAL1:def 12;
hence q . i = eval ((poly_shift (p,(i + 1))),r) by A3
.= eval ((0_. L),r) by A10, Th40
.= 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 A5, A6, ALGSEQ_1:10;
reconsider q = q as AlgSequence of L by A9, ALGSEQ_1:def 1;
A12: lq1 = ((len p) -' 1) -' 1 by A8, NAT_D:34;

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 A15, A16, NAT_1:13;
then ((len p) -' 1) -' 1 >= m by A16, NAT_D:34;
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 = H₁(k) ) )
(len p) -' 1 is_at_least_length_of q by A9, ALGSEQ_1:def 2;
hence (len q) + 1 = ((p1 + 1) -' 1) + 1 by A5, A13, ALGSEQ_1:def 3
.= len p by A5, NAT_D:34 ;
:: thesis: for k being Nat holds q . k = H₁(k)
let k be Nat; :: thesis: q . k = H₁(k)
k in NAT by ORDINAL1:def 12;
hence q . k = H₁(k) by A3; :: thesis: verum

end;

thus ( not len p > 0 implies ex b₁ being Polynomial of L st b₁ = 0_. L ) ; :: thesis: verum