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

( 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