:: deftheorem Def12 defines CCod COH_SP:def 12 :
for X being set
for b₂ being Function of (MapsC X),(CSp X) holds
( b₂ = CCod X iff for l being Element of MapsC X holds b₂ . l = cod l );