( p <> 0_. L & q <> 0_. L ) by Def5;
then p *' q <> 0_. L by Th23;
hence p *' q is non-zero by Def5; :: thesis: verum