(
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