for f, g being non empty Element of HFuncs NAT
for F being with_the_same_arity FinSequence of HFuncs NAT st g = f * <:F:> holds
arity g = arity F