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