let L be non trivial right_complementable distributive Abelian add-associative right_zeroed unital domRing-like left_zeroed doubleLoopStr ; :: thesis: for p1, p2 being Polynomial of L holds
( not p1 *' p2 = 0_. L or p1 = 0_. L or p2 = 0_. L )
let p1, p2 be Polynomial of L; :: thesis: ( not p1 *' p2 = 0_. L or p1 = 0_. L or p2 = 0_. L )
assume A1: p1 *' p2 = 0_. L ; :: thesis: ( p1 = 0_. L or p2 = 0_. L )
now :: thesis: ( p1 <> 0_. L implies not p2 <> 0_. L )
assume ( p1 <> 0_. L & p2 <> 0_. L ) ; :: thesis: contradiction
then reconsider x1 = p1, x2 = p2 as non zero Polynomial of L by UPROOTS:def 5;
not x1 *' x2 is zero ;
hence contradiction by A1; :: thesis: verum
end;
hence ( p1 = 0_. L or p2 = 0_. L ) ; :: thesis: verum