consider G, H being AddGroup;
set z = ZERO G,H;
fun (ZERO G,H) is additive ;
then ZERO G,H is GroupMorphism-like by Def18;
hence ex b₁ being GroupMorphismStr st
( b₁ is strict & b₁ is GroupMorphism-like ) ; :: thesis: verum