let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for p, q being Polynomial of L st ( len p = 0 or len q = 0 ) holds

len (p *' q) = 0

let p, q be Polynomial of L; :: thesis: ( ( len p = 0 or len q = 0 ) implies len (p *' q) = 0 )

assume A1: ( len p = 0 or len q = 0 ) ; :: thesis: len (p *' q) = 0

len (p *' q) = 0

let p, q be Polynomial of L; :: thesis: ( ( len p = 0 or len q = 0 ) implies len (p *' q) = 0 )

assume A1: ( len p = 0 or len q = 0 ) ; :: thesis: len (p *' q) = 0