theorem Th14: :: E_TRANS2:2

for p1, q1 being sequence of INT.Ring holds (p1 *' q1) . 0 = (p1 . 0) * (q1 . 0)