theorem Th3: :: RINGCAT1:3

for F being strict RingMorphism holds
( F is Morphism of dom F, cod F & dom F <= cod F )