let L be non empty right_complementable associative commutative well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for p1, p2 being Polynomial of L st p1 <> 0_. L & p2 <> 0_. L holds
deg (p1 *' p2) = (deg p1) + (deg p2)
let p1, p2 be Polynomial of L; :: thesis: ( p1 <> 0_. L & p2 <> 0_. L implies deg (p1 *' p2) = (deg p1) + (deg p2) )
assume A1: ( p1 <> 0_. L & p2 <> 0_. L ) ; :: thesis: deg (p1 *' p2) = (deg p1) + (deg p2)
A2: ( dom p1 = NAT & dom p2 = NAT ) by FUNCT_2:def 1;
( deg p1 is Element of NAT & deg p2 is Element of NAT ) by A1, Lm9;
then A3: ( p1 /. (deg p1) = p1 . (deg p1) & p2 /. (deg p2) = p2 . (deg p2) ) by A2, PARTFUN1:def 8;
( len p1 <> 0 & len p2 <> 0 ) by A1, POLYNOM4:8;
then ( len p1 > 0 & len p2 > 0 ) ;
then ( (len p1) + 1 > 0 + 1 & (len p2) + 1 > 0 + 1 ) by XREAL_1:8;
then ( len p1 >= 1 & len p2 >= 1 ) by NAT_1:13;
then ( (len p1) - 1 >= 1 - 1 & (len p2) - 1 >= 1 - 1 ) by XREAL_1:11;
then A4: ( p1 /. (deg p1) = p1 . ((len p1) -' 1) & p2 /. (deg p2) = p2 . ((len p2) -' 1) ) by A3, XREAL_0:def 2;
( deg p1 <> - 1 & deg p2 <> - 1 ) by A1, Th20;
then ( p1 /. (deg p1) <> 0. L & p2 /. (deg p2) <> 0. L ) by A3, Lm8;
then (p1 . ((len p1) -' 1)) * (p2 . ((len p2) -' 1)) <> 0. L by A4, VECTSP_2:def 5;
hence deg (p1 *' p2) = (((len p1) + (len p2)) - 1) - 1 by POLYNOM4:13
.= (deg p1) + (deg p2) ;
:: thesis: verum