theorem mm5: :: FIELD_14:66

for R being non degenerated comRing
for p being Element of the carrier of (Polynom-Ring R)
for S being comRingExtension of R
for q being Element of the carrier of (Polynom-Ring S) st q = p holds
(Deriv S) . q = (Deriv R) . p