for P being non empty primitive-recursively_closed Subset of (HFuncs NAT)
for f being Element of P
for F being with_the_same_arity FinSequence of P st arity f = len F holds
f * <:F:> in P