let R be Field; :: thesis: for p, q being Polynomial of R holds len (p *' q) <= ((len p) + (len q)) -' 1
let p, q be Polynomial of R; :: thesis: len (p *' q) <= ((len p) + (len q)) -' 1
((len p) + (len q)) -' 1 is_at_least_length_of p *' q

proof

now :: thesis: for i being Nat st i >= ((len p) + (len q)) -' 1 holds
(p *' q) . i = 0. R

let i be Nat; :: thesis: ( i >= ((len p) + (len q)) -' 1 implies (p *' q) . i = 0. R )
i in NAT by ORDINAL1:def 12;
then consider r being FinSequence of the carrier of R such that
A2: len r = i + 1 and
A3: (p *' q) . i = Sum r and
A4: for k being Element of NAT st k in dom r holds
r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by POLYNOM3:def 9;
assume i >= ((len p) + (len q)) -' 1 ; :: thesis: (p *' q) . i = 0. R
then i >= ((len p) + (len q)) - 1 by XREAL_0:def 2;
then i + 1 >= (len p) + (len q) by XREAL_1:20;
then A5: - (len p) >= - ((i + 1) - (len q)) by XREAL_1:24, XREAL_1:19;

now :: thesis: for k being Element of NAT st k in dom r holds
r . k = 0. R

let k be Element of NAT ; :: thesis: ( k in dom r implies r . b₁ = 0. R )
assume A6: k in dom r ; :: thesis: r . b₁ = 0. R
then A7: r . k = (p . (k -' 1)) * (q . ((i + 1) -' k)) by A4;
k in Seg (len r) by A6, FINSEQ_1:def 3;
then A8: k <= i + 1 by A2, FINSEQ_1:1;

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

suppose k -' 1 < len p ; :: thesis: r . b₁ = 0. R

then k - 1 < len p by XREAL_0:def 2;
then - (k - 1) > - (len p) by XREAL_1:24;
then 1 - k > (len q) - (i + 1) by A5, XXREAL_0:2;
then (i + 1) + (1 - k) > len q by XREAL_1:19;
then ((i + 1) - k) + 1 > len q ;
then ((i + 1) -' k) + 1 > len q by A8, XREAL_1:48, XREAL_0:def 2;
then q . ((i + 1) -' k) = 0. R by NAT_1:13, ALGSEQ_1:8;
hence r . k = 0. R by A7; :: thesis: verum

end;

suppose k -' 1 >= len p ; :: thesis: r . b₁ = 0. R

then p . (k -' 1) = 0. R by ALGSEQ_1:8;
hence r . k = 0. R by A7; :: thesis: verum

end;

end;

end;

hence (p *' q) . i = 0. R by A3, POLYNOM3:1; :: thesis: verum

end;

hence ((len p) + (len q)) -' 1 is_at_least_length_of p *' q ; :: thesis: verum

end;

hence len (p *' q) <= ((len p) + (len q)) -' 1 by ALGSEQ_1:def 3; :: thesis: verum