:: deftheorem defines dom COH_SP:def 7 :
for X being set
for l being Element of MapsC X holds dom l = (l `1) `1 ;