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
per cases ( len p = 0 or len q = 0 ) by A1;
suppose len p = 0 ; :: thesis: len (p *' q) = 0
then p = 0_. L by POLYNOM4:5;
then p *' q = 0_. L by POLYNOM4:2;
hence len (p *' q) = 0 by POLYNOM4:3; :: thesis: verum
end;
suppose len q = 0 ; :: thesis: len (p *' q) = 0
then q = 0_. L by POLYNOM4:5;
then p *' q = 0_. L by Th17;
hence len (p *' q) = 0 by POLYNOM4:3; :: thesis: verum
end;
end;