:: deftheorem Def25 defines fCod COH_SP:def 26 :
for X being set
for b₂ being Function of (MapsT X),(TOL X) holds
( b₂ = fCod X iff for m being Element of MapsT X holds b₂ . m = cod m );