let L be non empty right_complementable well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ; :: thesis: for p, q being Polynomial of L st (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L holds
0 < len (p *' q)
let p, q be Polynomial of L; :: thesis: ( (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L implies 0 < len (p *' q) )
assume A1: (p . ((len p) -' 1)) * (q . ((len q) -' 1)) <> 0. L ; :: thesis: 0 < len (p *' q)
now :: thesis: not len q <= 0
assume len q <= 0 ; :: thesis: contradiction
then len q = 0 ;
then q = 0_. L by POLYNOM4:5;
then q . ((len q) -' 1) = 0. L by FUNCOP_1:7;
hence contradiction by A1; :: thesis: verum
end;
then A2: 0 + 1 <= len q by NAT_1:13;
now :: thesis: not len p <= 0
assume len p <= 0 ; :: thesis: contradiction
then len p = 0 ;
then p = 0_. L by POLYNOM4:5;
then p . ((len p) -' 1) = 0. L by FUNCOP_1:7;
hence contradiction by A1; :: thesis: verum
end;
then 0 + 1 <= len p by NAT_1:13;
then (len p) + (len q) >= 1 + 1 by A2, XREAL_1:7;
then ((len p) + (len q)) - 1 >= (1 + 1) - 1 by XREAL_1:9;
hence 0 < len (p *' q) by A1, POLYNOM4:10; :: thesis: verum