let G be Ring; :: thesis: ex F being RingMorphism st
( dom F = G & cod F = G )
set i = ID G;
take ID G ; :: thesis: ( dom (ID G) = G & cod (ID G) = G )
thus ( dom (ID G) = G & cod (ID G) = G ) ; :: thesis: verum