( LC p = 1. L & LC q = 1. L ) by RATFUNC1:def 7;
hence 1. L = (LC p) * (LC q)
.= LC (p *' q) by Th44 ;
:: according to RATFUNC1:def 7 :: thesis: verum