[STATEMENT]
lemma Seq_iff: "Seq r d \<longleftrightarrow> d \<le> hdomain r \<and> hfun_sigma r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Seq r d = (d \<le> hdomain r \<and> hfun_sigma r)
[PROOF STEP]
by (auto simp: Seq_def hfun_sigma_iff)