( 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