hereby :: thesis: ( not len p > 0 implies ex b_{1} being Polynomial of L st b_{1} = 0_. L )

thus
( not len p > 0 implies ex b
r in Roots p
by A1, POLYNOM5:def 10;

then A2: len p <> 1 by Th43;

deffunc H_{1}( 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_{1}(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_{1}(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;

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;

_{1}(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_{1}(k)

let k be Nat; :: thesis: q . k = H_{1}(k)

k in NAT by ORDINAL1:def 12;

hence q . k = H_{1}(k)
by A3; :: thesis: verum

end;then A2: len p <> 1 by Th43;

deffunc H

set lq = (len p) -' 1;

consider q being sequence of L such that

A3: for k being Element of NAT holds q . k = H

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

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

reconsider lq1 = lq1 as Element of NAT by ORDINAL1:def 12;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;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

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

take q = q; :: thesis: ( (len q) + 1 = len p & ( for k being Nat holds q . k = Hnot (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;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

(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

let k be Nat; :: thesis: q . k = H

k in NAT by ORDINAL1:def 12;

hence q . k = H