for F being with_the_same_arity FinSequence st len F = 0 holds
arity F = 0