let L be non empty right_complementable well-unital distributive add-associative right_zeroed associative commutative domRing-like doubleLoopStr ; :: thesis: for p, q being Polynomial of L st len p > 0 & len q > 0 holds
len (p *' q) <= (len p) + (len q)
let p, q be Polynomial of L; :: thesis: ( len p > 0 & len q > 0 implies len (p *' q) <= (len p) + (len q) )
assume that
A1: len p > 0 and
A2: len q > 0 ; :: thesis: len (p *' q) <= (len p) + (len q)
A3: ((len p) + (len q)) - 1 <= ((len p) + (len q)) - 0 by XREAL_1:13;
(len q) + 1 > 0 + 1 by A2, XREAL_1:6;
then len q >= 1 by NAT_1:13;
then A4: (len q) - 1 >= 1 - 1 by XREAL_1:13;
q . ((len q) - 1) <> 0. L by A2, Th8;
then A5: q . ((len q) -' 1) <> 0. L by A4, XREAL_0:def 2;
(len p) + 1 > 0 + 1 by A1, XREAL_1:6;
then len p >= 1 by NAT_1:13;
then A6: (len p) - 1 >= 1 - 1 by XREAL_1:13;
p . ((len p) - 1) <> 0. L by A1, Th8;
then p . ((len p) -' 1) <> 0. L by A6, XREAL_0:def 2;
then (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L by A5, VECTSP_2:def 1;
hence len (p *' q) <= (len p) + (len q) by A3, POLYNOM4:10; :: thesis: verum