let F be with_the_same_arity FinSequence; :: thesis: ( len F = 0 implies arity F = 0 )
assume len F = 0 ; :: thesis: arity F = 0
then F = {} ;
then for f being homogeneous Function holds not f in rng F ;
hence arity F = 0 by Def4; :: thesis: verum