:: deftheorem defines composition-closure COMPUT_1:def 19 :
for Q being Subset of (HFuncs NAT) holds composition-closure Q = Q \/ { (f * <:F:>) where f is Element of HFuncs NAT, F is with_the_same_arity Element of (HFuncs NAT) * : ( f in Q & arity f = len F & rng F c= Q ) } ;