for x being FinSequence holds not x in dom {} ;
hence arity {} = 0 by MARGREL1:def 25; :: thesis: verum