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

assume A2: 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
A3: len p = p1 + 1 by NAT_1:6;
set lq = (len p) -' 1;
A4: (len p) -' 1 = p1 by A3, NAT_D:34;
A5: len p >= 0 + 1 by A2, NAT_1:13;
r in Roots p by A1, POLYNOM5:def 9;
then len p <> 1 by Th48;
then consider lq1 being Nat such that
A6: (len p) -' 1 = lq1 + 1 by A3, A4, A5, NAT_1:6;
reconsider lq1 = lq1 as Element of NAT by ORDINAL1:def 13;
A7: lq1 = ((len p) -' 1) -' 1 by A6, NAT_D:34;
A8: (len p) -' 1 < len p by A3, A4, NAT_1:13;
deffunc H₁( Nat) -> Element of the carrier of L = eval (poly_shift p,($1 + 1)),r;
consider q being sequence of L such that
A9: for k being Element of NAT holds q . k = H₁(k) from FUNCT_2:sch 4();
reconsider q = q as sequence of L ;
q . lq1 = eval (poly_shift p,(lq1 + 1)),r by A9
.= (r * (eval (poly_shift p,(len p)),r)) + (p . ((len p) -' 1)) by A3, A4, A6, A8, Th47
.= (r * (eval (0_. L),r)) + (p . ((len p) -' 1)) by Th45
.= (r * (0. L)) + (p . ((len p) -' 1)) by POLYNOM4:20
.= (0. L) + (p . ((len p) -' 1)) by VECTSP_1:36
.= p . ((len p) -' 1) by RLVECT_1:10 ;
then A10: q . lq1 <> 0. L by A3, A4, ALGSEQ_1:25;

A11: now

let i be Nat; :: thesis: ( i >= (len p) -' 1 implies q . i = 0. L )
assume A12: i >= (len p) -' 1 ; :: thesis: q . i = 0. L
i >= p1 by A3, A12, NAT_D:34;
then A13: i + 1 >= len p by A3, XREAL_1:8;
i in NAT by ORDINAL1:def 13;
hence q . i = eval (poly_shift p,(i + 1)),r by A9
.= eval (0_. L),r by A13, Th45
.= 0. L by POLYNOM4:20 ;
:: thesis: verum

end;

then reconsider q = q as AlgSequence of L by ALGSEQ_1:def 2;
take q = q; :: thesis: ( (len q) + 1 = len p & ( for k being Nat holds q . k = H₁(k) ) )
A14: (len p) -' 1 is_at_least_length_of q by A11, ALGSEQ_1:def 3;

now

let m be Nat; :: thesis: ( m is_at_least_length_of q implies not (len p) -' 1 > m )
assume A15: m is_at_least_length_of q ; :: thesis: not (len p) -' 1 > m
assume A16: (len p) -' 1 > m ; :: thesis: contradiction
then consider lq1 being Nat such that
A17: (len p) -' 1 = lq1 + 1 by NAT_1:6;
lq1 >= m by A16, A17, NAT_1:13;
then ((len p) -' 1) -' 1 >= m by A17, NAT_D:34;
hence contradiction by A7, A10, A15, ALGSEQ_1:def 3; :: thesis: verum

end;

hence (len q) + 1 = ((p1 + 1) -' 1) + 1 by A3, A14, ALGSEQ_1:def 4
.= len p by A3, 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 13;
hence q . k = H₁(k) by A9; :: thesis: verum

end;

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