take ZERO (G,H) ; :: thesis: ( dom (ZERO (G,H)) = G & cod (ZERO (G,H)) = H )
thus ( dom (ZERO (G,H)) = G & cod (ZERO (G,H)) = H ) ; :: thesis: verum