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