let L be non empty right_complementable associative commutative well-unital distributive add-associative right_zeroed 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 A1: ( len p > 0 & len q > 0 ) ; :: thesis: len (p *' q) <= (len p) + (len q)
then A2: ( p . ((len p) - 1) <> 0. L & q . ((len q) - 1) <> 0. L ) by Th8;
( (len p) + 1 > 0 + 1 & (len q) + 1 > 0 + 1 ) by A1, XREAL_1:8;
then ( len p >= 1 & len q >= 1 ) by NAT_1:13;
then ( (len p) - 1 >= 1 - 1 & (len q) - 1 >= 1 - 1 ) by XREAL_1:15;
then ( p . ((len p) -' 1) <> 0. L & q . ((len q) -' 1) <> 0. L ) by A2, XREAL_0:def 2;
then A3: (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L by VECTSP_2:def 5;
((len p) + (len q)) - 1 <= ((len p) + (len q)) - 0 by XREAL_1:15;
hence len (p *' q) <= (len p) + (len q) by A3, POLYNOM4:13; :: thesis: verum