:: deftheorem defines FuncsT COH_SP:def 19 :
for X being set holds FuncsT X = union { (Funcs ((T `2),(TT `2))) where T, TT is Element of TOL X : verum } ;