:: deftheorem defines dom COH_SP:def 21 :
for X being set
for m being Element of MapsT X holds dom m = (m `1) `1 ;