:: deftheorem defines FuncsC COH_SP:def 5 :
for X being set holds FuncsC X = union { (Funcs ((union x),(union y))) where x, y is Element of CSp X : verum } ;