:: deftheorem Def26 defines fComp COH_SP:def 27 :
for X being set
for b₂ being PartFunc of [:(MapsT X),(MapsT X):],(MapsT X) holds
( b₂ = fComp X iff ( ( for m2, m1 being Element of MapsT X holds
( [m2,m1] in dom b₂ iff dom m2 = cod m1 ) ) & ( for m2, m1 being Element of MapsT X st dom m2 = cod m1 holds
b₂ . [m2,m1] = m2 * m1 ) ) );