let L be non empty right_complementable well-unital distributive add-associative right_zeroed associative domRing-like doubleLoopStr ; 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; ( p1 <> 0_. L & p2 <> 0_. L implies deg (p1 *' p2) = (deg p1) + (deg p2) )
assume that
A1:
p1 <> 0_. L
and
A2:
p2 <> 0_. L
; deg (p1 *' p2) = (deg p1) + (deg p2)
A3:
dom p2 = NAT
by FUNCT_2:def 1;
deg p2 is Element of NAT
by A2, Lm8;
then A4:
p2 /. (deg p2) = p2 . (deg p2)
by A3, PARTFUN1:def 6;
deg p2 <> - 1
by A2, Th20;
then A5:
p2 /. (deg p2) <> 0. L
by A4, Lm7;
A6:
dom p1 = NAT
by FUNCT_2:def 1;
deg p1 is Element of NAT
by A1, Lm8;
then A7:
p1 /. (deg p1) = p1 . (deg p1)
by A6, PARTFUN1:def 6;
len p2 <> 0
by A2, POLYNOM4:5;
then
(len p2) + 1 > 0 + 1
by XREAL_1:6;
then
len p2 >= 1
by NAT_1:13;
then
(len p2) - 1 >= 1 - 1
by XREAL_1:9;
then A8:
p2 /. (deg p2) = p2 . ((len p2) -' 1)
by A4, XREAL_0:def 2;
deg p1 <> - 1
by A1, Th20;
then A9:
p1 /. (deg p1) <> 0. L
by A7, Lm7;
len p1 <> 0
by A1, POLYNOM4:5;
then
(len p1) + 1 > 0 + 1
by XREAL_1:6;
then
len p1 >= 1
by NAT_1:13;
then
(len p1) - 1 >= 1 - 1
by XREAL_1:9;
then
p1 /. (deg p1) = p1 . ((len p1) -' 1)
by A7, XREAL_0:def 2;
then
(p1 . ((len p1) -' 1)) * (p2 . ((len p2) -' 1)) <> 0. L
by A8, A9, A5, VECTSP_2:def 1;
hence deg (p1 *' p2) =
(((len p1) + (len p2)) - 1) - 1
by POLYNOM4:10
.=
(deg p1) + (deg p2)
;
verum