:: deftheorem Def11 defines CDom COH_SP:def 11 :
for X being set
for b₂ being Function of (MapsC X),(CSp X) holds
( b₂ = CDom X iff for l being Element of MapsC X holds b₂ . l = dom l );