set PRL = Polynom-Ring L;
let x, y be Element of (Polynom-Ring L); :: according to VECTSP_2:def 1 :: thesis: ( not x * y = 0. (Polynom-Ring L) or x = 0. (Polynom-Ring L) or y = 0. (Polynom-Ring L) )
reconsider xp = x, yp = y as Polynomial of L by POLYNOM3:def 10;
A1: 0_. L = 0. (Polynom-Ring L) by POLYNOM3:def 10;
assume x * y = 0. (Polynom-Ring L) ; :: thesis: ( x = 0. (Polynom-Ring L) or y = 0. (Polynom-Ring L) )
then xp *' yp = 0_. L by A1, POLYNOM3:def 10;
hence ( x = 0. (Polynom-Ring L) or y = 0. (Polynom-Ring L) ) by A1, Th18; :: thesis: verum