theorem Th11: :: POLYNOM4:11

for L being non empty ZeroStr
for p being Polynomial of L holds Leading-Monomial p = (0_. L) +* (((len p) -' 1),(p . ((len p) -' 1)))