let L be non empty ZeroStr ; :: thesis: for p being Polynomial of L st p <> 0_. L holds
len (p || ((len p) -' 1)) < len p
let p be Polynomial of L; :: thesis: ( p <> 0_. L implies len (p || ((len p) -' 1)) < len p )
assume A1: p <> 0_. L ; :: thesis: len (p || ((len p) -' 1)) < len p
set m = (len p) -' 1;
A2: (len p) -' 1 = (len p) - 1 by A1, Th22;
A3: (len p) - 1 < (len p) - 0 by XREAL_1:15;
len p is_at_least_length_of p || ((len p) -' 1)

proof

let i be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not len p <= i or (p || ((len p) -' 1)) . i = 0. L )
assume A4: i >= len p ; :: thesis: (p || ((len p) -' 1)) . i = 0. L
thus (p || ((len p) -' 1)) . i = p . i by A2, A3, A4, FUNCT_7:32
.= 0. L by A4, ALGSEQ_1:8 ; :: thesis: verum

end;

then A5: len (p || ((len p) -' 1)) <= len p by ALGSEQ_1:def 3;

now :: thesis: not len (p || ((len p) -' 1)) = len p

assume len (p || ((len p) -' 1)) = len p ; :: thesis: contradiction
then A6: len (p || ((len p) -' 1)) is_at_least_length_of p by ALGSEQ_1:def 3;
(len p) -' 1 is_at_least_length_of p || ((len p) -' 1)

proof

let i be Nat; :: according to ALGSEQ_1:def 2 :: thesis: ( not (len p) -' 1 <= i or (p || ((len p) -' 1)) . i = 0. L )
assume A7: i >= (len p) -' 1 ; :: thesis: (p || ((len p) -' 1)) . i = 0. L

per cases ( i <> (len p) -' 1 or i = (len p) -' 1 ) ;

suppose A8: i <> (len p) -' 1 ; :: thesis: (p || ((len p) -' 1)) . i = 0. L

then i > (len p) -' 1 by A7, XXREAL_0:1;
then i >= ((len p) - 1) + 1 by A2, NAT_1:13;
hence 0. L = p . i by ALGSEQ_1:8
.= (p || ((len p) -' 1)) . i by A8, FUNCT_7:32 ;
:: thesis: verum

end;

suppose i = (len p) -' 1 ; :: thesis: (p || ((len p) -' 1)) . i = 0. L

hence (p || ((len p) -' 1)) . i = 0. L by Th32; :: thesis: verum

end;

end;

end;

then (len p) -' 1 >= len (p || ((len p) -' 1)) by ALGSEQ_1:def 3;
then A9: p . ((len p) -' 1) = 0. L by A6;
len p <> 0 by A1, POLYNOM4:5;
hence contradiction by A9, UPROOTS:18; :: thesis: verum

end;

hence len (p || ((len p) -' 1)) < len p by A5, XXREAL_0:1; :: thesis: verum