theorem Th27: :: E_TRANS1:27

for p, q being Element of the carrier of (Polynom-Ring INT.Ring) holds
( ^ (p + q) = (^ p) + (^ q) & ^ (p * q) = (^ p) * (^ q) )