A function elimination method for checking satisfiability of arithmetical logics