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 1 < len p & 1 < len q holds
len p < len (p *' q)
let p, q be Polynomial of L; :: thesis: ( 1 < len p & 1 < len q implies len p < len (p *' q) )
assume that
A1: 1 < len p and
A2: 1 < len q ; :: thesis: len p < len (p *' q)
( p . ((len p) -' 1) <> 0. L & q . ((len q) -' 1) <> 0. L ) by A1, A2, Th15;
then (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L by VECTSP_2:def 1;
then A3: len (p *' q) = ((len p) + (len q)) - 1 by POLYNOM4:10;
(len q) - 1 > 1 - 1 by A2, XREAL_1:14;
then (len p) + ((len q) - 1) > 0 + (len p) by XREAL_1:8;
hence len p < len (p *' q) by A3; :: thesis: verum