set G = the Ring;
take {(ID the Ring)} ; :: thesis: {(ID the Ring)} is RingMorphism_DOMAIN-like
for x being object st x in {(ID the Ring)} holds
x is strict RingMorphism by TARSKI:def 1;
hence {(ID the Ring)} is RingMorphism_DOMAIN-like ; :: thesis: verum