let L be non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for p, q being Polynomial of L holds len (p *' q) <= ((len p) + (len q)) -' 1

let p, q be Polynomial of L; :: thesis: len (p *' q) <= ((len p) + (len q)) -' 1

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

let p, q be Polynomial of L; :: thesis: len (p *' q) <= ((len p) + (len q)) -' 1

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

(p *' q) . i = 0. L

then
((len p) + (len q)) -' 1 is_at_least_length_of p *' q
by ALGSEQ_1:def 2;(p *' q) . i = 0. L

let i be Nat; :: thesis: ( i >= ((len p) + (len q)) -' 1 implies (p *' q) . i = 0. L )

A1: ((len p) + (len q)) -' 1 >= ((len p) + (len q)) - 1 by XREAL_0:def 2;

i in NAT by ORDINAL1:def 12;

then consider r being FinSequence of the carrier of L 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. L

then i >= (len p) + ((len q) - 1) by A1, XXREAL_0:2;

then len p <= i - ((len q) - 1) by XREAL_1:19;

then A5: - (len p) >= - ((i - (len q)) + 1) by XREAL_1:24;

end;A1: ((len p) + (len q)) -' 1 >= ((len p) + (len q)) - 1 by XREAL_0:def 2;

i in NAT by ORDINAL1:def 12;

then consider r being FinSequence of the carrier of L 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. L

then i >= (len p) + ((len q) - 1) by A1, XXREAL_0:2;

then len p <= i - ((len q) - 1) by XREAL_1:19;

then A5: - (len p) >= - ((i - (len q)) + 1) by XREAL_1:24;

now :: thesis: for k being Element of NAT st k in dom r holds

r . k = 0. L

hence
(p *' q) . i = 0. L
by A3, POLYNOM3:1; :: thesis: verumr . k = 0. L

let k be Element of NAT ; :: thesis: ( k in dom r implies r . b_{1} = 0. L )

assume A6: k in dom r ; :: thesis: r . b_{1} = 0. L

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 k <= i + 1 by A2, FINSEQ_1:1;

then A8: (i + 1) - k >= 0 by XREAL_1:48;

end;assume A6: k in dom r ; :: thesis: r . b

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 k <= i + 1 by A2, FINSEQ_1:1;

then A8: (i + 1) - k >= 0 by XREAL_1:48;

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

end;

suppose
k -' 1 < len p
; :: thesis: r . b_{1} = 0. L

then
k - 1 < len p
by XREAL_0:def 2;

then - (k - 1) > - (len p) by XREAL_1:24;

then 1 - k > ((len q) - 1) - i by A5, XXREAL_0:2;

then i + (1 - k) > (len q) - 1 by XREAL_1:19;

then (i + 1) -' k > (len q) - 1 by A8, XREAL_0:def 2;

then (i + 1) -' k >= ((len q) - 1) + 1 by INT_1:7;

then q . ((i + 1) -' k) = 0. L by ALGSEQ_1:8;

hence r . k = 0. L by A7; :: thesis: verum

end;then - (k - 1) > - (len p) by XREAL_1:24;

then 1 - k > ((len q) - 1) - i by A5, XXREAL_0:2;

then i + (1 - k) > (len q) - 1 by XREAL_1:19;

then (i + 1) -' k > (len q) - 1 by A8, XREAL_0:def 2;

then (i + 1) -' k >= ((len q) - 1) + 1 by INT_1:7;

then q . ((i + 1) -' k) = 0. L by ALGSEQ_1:8;

hence r . k = 0. L by A7; :: thesis: verum

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