( dom (ZERO (G,H)) = G & cod (ZERO (G,H)) = H ) ;
then reconsider z = ZERO (G,H) as Morphism of G,H by Def8;
take z ; :: thesis: z is strict
thus z is strict ; :: thesis: verum