:: deftheorem defines MapsT COH_SP:def 20 :
for X being set holds MapsT X = { [[T,TT],f] where T, TT is Element of TOL X, f is Element of FuncsT X : ( ( TT `2 = {} implies T `2 = {} ) & f is Function of (T `2),(TT `2) & ( for x, y being set st [x,y] in T `1 holds
[(f . x),(f . y)] in TT `1 ) ) } ;