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

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