:: deftheorem Def18 defines MapsSet GRCAT_1:def 20 :
for G, H being 1-sorted
for b₃ being set holds
( b₃ is MapsSet of G,H iff for x being set st x in b₃ holds
x is Function of G,H );