let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p, q being Polynomial of L st p *' q is non-zero holds
( p is non-zero & q is non-zero )
let p, q be Polynomial of L; :: thesis: ( p *' q is non-zero implies ( p is non-zero & q is non-zero ) )
assume that
A1: p *' q is non-zero and
A2: ( not p is non-zero or not q is non-zero ) ; :: thesis: contradiction
( len p = 0 or len q = 0 ) by A2, Th14;
then len (p *' q) = 0 by Th30;
hence contradiction by A1, Th14; :: thesis: verum