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 object 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 ) ; :: thesis: verum