let f be strict GroupMorphism; :: thesis: {f} is GroupMorphism_DOMAIN
for x being object st x in {f} holds
x is strict GroupMorphism by TARSKI:def 1;
hence {f} is GroupMorphism_DOMAIN by Def16; :: thesis: verum