( dom (ZERO (G,H)) = G & cod (ZERO (G,H)) = H ) ;
then ZERO (G,H) is Morphism of G,H by Def19;
hence ex b₁ being Morphism of G,H st b₁ is strict ; :: thesis: verum