theorem :: FIELD_4:4

for R being comRing holds R is comRingExtension of R