:: deftheorem defines ZeroMap GRCAT_1:def 7 :
for G being non empty 1-sorted
for H being non empty ZeroStr holds ZeroMap (G,H) = the carrier of G --> (0. H);