:: deftheorem Def13 defines CComp COH_SP:def 13 :
for X being set
for b₂ being PartFunc of [:(MapsC X),(MapsC X):],(MapsC X) holds
( b₂ = CComp X iff ( ( for l2, l1 being Element of MapsC X holds
( [l2,l1] in dom b₂ iff dom l2 = cod l1 ) ) & ( for l2, l1 being Element of MapsC X st dom l2 = cod l1 holds
b₂ . [l2,l1] = l2 * l1 ) ) );