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 9;
then A1: len p <> 1 by Th46;
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
A2: for k being Element of NAT holds q . k = H₁(k) from FUNCT_2:sch 4();
reconsider q = q as sequence of L ;
assume A3: 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
A4: len p = p1 + 1 by NAT_1:6;
A5: (len p) -' 1 = p1 by A4, NAT_D:34;
then A6: (len p) -' 1 < len p by A4, NAT_1:13;
len p >= 0 + 1 by A3, NAT_1:13;
then consider lq1 being Nat such that
A7: (len p) -' 1 = lq1 + 1 by A4, A5, A1, NAT_1:6;

A8: 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 A4, NAT_D:34;
then A9: i + 1 >= len p by A4, XREAL_1:6;
i in NAT by ORDINAL1:def 12;
hence q . i = eval ((poly_shift (p,(i + 1))),r) by A2
.= eval ((0_. L),r) by A9, Th43
.= 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 A2
.= (r * (eval ((poly_shift (p,(len p))),r))) + (p . ((len p) -' 1)) by A4, A5, A7, A6, Th45
.= (r * (eval ((0_. L),r))) + (p . ((len p) -' 1)) by Th43
.= (r * (0. L)) + (p . ((len p) -' 1)) by POLYNOM4:17
.= (0. L) + (p . ((len p) -' 1)) by VECTSP_1:6
.= p . ((len p) -' 1) by RLVECT_1:4 ;
then A10: q . lq1 <> 0. L by A4, A5, ALGSEQ_1:10;
reconsider q = q as AlgSequence of L by A8, ALGSEQ_1:def 1;
A11: lq1 = ((len p) -' 1) -' 1 by A7, NAT_D:34;

A12: 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 A13: m is_at_least_length_of q ; :: thesis: not (len p) -' 1 > m
assume A14: (len p) -' 1 > m ; :: thesis: contradiction
then consider lq1 being Nat such that
A15: (len p) -' 1 = lq1 + 1 by NAT_1:6;
lq1 >= m by A14, A15, NAT_1:13;
then ((len p) -' 1) -' 1 >= m by A15, NAT_D:34;
hence contradiction by A11, A10, A13, 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 A8, ALGSEQ_1:def 2;
hence (len q) + 1 = ((p1 + 1) -' 1) + 1 by A4, A12, ALGSEQ_1:def 3
.= len p by A4, 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 A2; :: thesis: verum

end;

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