:: deftheorem defines composition_closed COMPUT_1:def 12 :
for X being set holds
( X is composition_closed iff for f being Element of HFuncs NAT
for F being with_the_same_arity FinSequence of HFuncs NAT st f in X & arity f = len F & rng F c= X holds
f * <:F:> in X );