set m = the Element of M;
the Element of M is strict GroupMorphism by Def23;
hence ex b₁ being Element of M st b₁ is strict ; :: thesis: verum