set G = the AddGroup;
set z = ZERO ( the AddGroup, the AddGroup);
ZERO ( the AddGroup, the AddGroup) is GroupMorphism-like ;
hence ex b₁ being GroupMorphismStr st
( b₁ is strict & b₁ is GroupMorphism-like ) ; :: thesis: verum