[STATEMENT]
lemma S\<^sub>i: "E(x\<cdot>y) \<^bold>\<rightarrow> (E x \<^bold>\<and> E y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E x \<^bold>\<and> E y \<^bold>\<leftarrow> E (x \<cdot> y)
[PROOF STEP]
using S\<^sub>i\<^sub>i
[PROOF STATE]
proof (prove)
using this:
(E ?x \<^bold>\<and> E ?y \<^bold>\<leftarrow> E (?x \<cdot> ?y)) \<^bold>\<and> (E ?x \<^bold>\<leftarrow> E (dom ?x)) \<^bold>\<and> (E ?y \<^bold>\<leftarrow> E (cod ?y))

goal (1 subgoal):
 1. E x \<^bold>\<and> E y \<^bold>\<leftarrow> E (x \<cdot> y)
[PROOF STEP]
by blast