let L be non degenerated right_complementable add-associative right_zeroed well-unital distributive associative domRing-like doubleLoopStr ; :: thesis: for p, q being Polynomial of L holds LC (p *' q) = (LC p) * (LC q)
let p, q be Polynomial of L; :: thesis: LC (p *' q) = (LC p) * (LC q)

per cases ( ( p <> 0_. L & q <> 0_. L ) or p is zero or q is zero ) ;

suppose AS: ( p <> 0_. L & q <> 0_. L ) ; :: thesis: LC (p *' q) = (LC p) * (LC q)

len (p *' q) = (deg (p *' q)) + 1
.= ((deg p) + (deg q)) + 1 by AS, HURWITZ:23
.= (((len p) - 1) + ((len q) - 1)) + 1 ;
hence LC (p *' q) = (p *' q) . ((((len p) + (len q)) - 1) -' 1)
.= (LC p) * (LC q) by AS, lemmul ;
:: thesis: verum

end;

suppose A30: p is zero ; :: thesis: LC (p *' q) = (LC p) * (LC q)

then p *' q = 0_. L by Th17;
hence LC (p *' q) = (0. L) * (LC q) by FUNCOP_1:7
.= (LC p) * (LC q) by A30, FUNCOP_1:7 ;
:: thesis: verum

end;

suppose A31: q is zero ; :: thesis: LC (p *' q) = (LC p) * (LC q)

then p *' q = 0_. L by POLYNOM3:34;
hence LC (p *' q) = (LC p) * (0. L) by FUNCOP_1:7
.= (LC p) * (LC q) by A31, FUNCOP_1:7 ;
:: thesis: verum

end;

end;