reconsider x1 = p1 as Element of (Polynom-Ring L) by POLYNOM3:def 10;
reconsider x2 = p2 as Element of (Polynom-Ring L) by POLYNOM3:def 10;
p1 <> 0_. L ;
then A1: x1 <> 0. (Polynom-Ring L) by POLYNOM3:def 10;
p2 <> 0_. L ;
then x2 <> 0. (Polynom-Ring L) by POLYNOM3:def 10;
then x1 * x2 <> 0. (Polynom-Ring L) by A1, VECTSP_2:def 1;
then p1 *' p2 <> 0. (Polynom-Ring L) by POLYNOM3:def 10;
then p1 *' p2 <> 0_. L by POLYNOM3:def 10;
hence not p1 *' p2 is zero ; :: thesis: verum