consider G being AddGroup;
take {(ID G)} ; :: thesis: ( {(ID G)} is GroupMorphism_DOMAIN-like & not {(ID G)} is empty )
for x being set st x in {(ID G)} holds
x is strict GroupMorphism by TARSKI:def 1;
hence ( {(ID G)} is GroupMorphism_DOMAIN-like & not {(ID G)} is empty ) by Def23; :: thesis: verum