[STATEMENT]
lemma (in domain) ring_iso_imp_img_domain:
  assumes "h \<in> ring_iso R S"
  shows "domain (S \<lparr> zero := h \<zero> \<rparr>)" (is "domain ?h_img")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain (S\<lparr>zero := h \<zero>\<rparr>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. domain (S\<lparr>zero := h \<zero>\<rparr>)
[PROOF STEP]
note aux = m_closed integral one_not_zero one_closed zero_closed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> carrier R; ?y \<in> carrier R\<rbrakk> \<Longrightarrow> ?x \<otimes> ?y \<in> carrier R
\<lbrakk>?a \<otimes> ?b = \<zero>; ?a \<in> carrier R; ?b \<in> carrier R\<rbrakk> \<Longrightarrow> ?a = \<zero> \<or> ?b = \<zero>
\<one> \<noteq> \<zero>
\<one> \<in> carrier R
\<zero> \<in> carrier R

goal (1 subgoal):
 1. domain (S\<lparr>zero := h \<zero>\<rparr>)
[PROOF STEP]
interpret h_img?: cring ?h_img
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cring (S\<lparr>zero := h \<zero>\<rparr>)
[PROOF STEP]
using ring_iso_imp_img_cring[OF assms]
[PROOF STATE]
proof (prove)
using this:
cring (S\<lparr>zero := h \<zero>\<rparr>)

goal (1 subgoal):
 1. cring (S\<lparr>zero := h \<zero>\<rparr>)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. domain (S\<lparr>zero := h \<zero>\<rparr>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domain (S\<lparr>zero := h \<zero>\<rparr>)
[PROOF STEP]
proof (unfold_locales)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<noteq> \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
 2. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
have "\<one>\<^bsub>?h_img\<^esub> = \<zero>\<^bsub>?h_img\<^esub> \<Longrightarrow> h \<one> = h \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<Longrightarrow> h \<one> = h \<zero>
[PROOF STEP]
using ring_iso_memE(4)[OF assms]
[PROOF STATE]
proof (prove)
using this:
h \<one> = \<one>\<^bsub>S\<^esub>

goal (1 subgoal):
 1. \<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<Longrightarrow> h \<one> = h \<zero>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<Longrightarrow> h \<one> = h \<zero>

goal (2 subgoals):
 1. \<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<noteq> \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
 2. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<Longrightarrow> h \<one> = h \<zero>

goal (2 subgoals):
 1. \<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<noteq> \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
 2. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
have "h \<one> \<noteq> h \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<one> \<noteq> h \<zero>
[PROOF STEP]
using ring_iso_memE(5)[OF assms] aux(3-4)
[PROOF STATE]
proof (prove)
using this:
bij_betw h (carrier R) (carrier S)
\<one> \<noteq> \<zero>
\<one> \<in> carrier R

goal (1 subgoal):
 1. h \<one> \<noteq> h \<zero>
[PROOF STEP]
unfolding bij_betw_def inj_on_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. h x = h y \<longrightarrow> x = y) \<and> h ` carrier R = carrier S
\<one> \<noteq> \<zero>
\<one> \<in> carrier R

goal (1 subgoal):
 1. h \<one> \<noteq> h \<zero>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
h \<one> \<noteq> h \<zero>

goal (2 subgoals):
 1. \<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<noteq> \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
 2. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<Longrightarrow> h \<one> = h \<zero>
h \<one> \<noteq> h \<zero>
[PROOF STEP]
show "\<one>\<^bsub>?h_img\<^esub> \<noteq> \<zero>\<^bsub>?h_img\<^esub>"
[PROOF STATE]
proof (prove)
using this:
\<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<Longrightarrow> h \<one> = h \<zero>
h \<one> \<noteq> h \<zero>

goal (1 subgoal):
 1. \<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<noteq> \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<one>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<noteq> \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
assume A: "a \<otimes>\<^bsub>?h_img\<^esub> b = \<zero>\<^bsub>?h_img\<^esub>" "a \<in> carrier ?h_img" "b \<in> carrier ?h_img"
[PROOF STATE]
proof (state)
this:
a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)
b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)
b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)
[PROOF STEP]
obtain r1 r2
      where r1: "r1 \<in> carrier R" "a = h r1"
        and r2: "r2 \<in> carrier R" "b = h r2"
[PROOF STATE]
proof (prove)
using this:
a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)
b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)

goal (1 subgoal):
 1. (\<And>r1 r2. \<lbrakk>r1 \<in> carrier R; a = h r1; r2 \<in> carrier R; b = h r2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms image_iff[where ?f = h and ?A = "carrier R"]
[PROOF STATE]
proof (prove)
using this:
a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)
b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)
h \<in> ring_iso R S
(?z \<in> h ` carrier R) = (\<exists>x\<in>carrier R. ?z = h x)

goal (1 subgoal):
 1. (\<And>r1 r2. \<lbrakk>r1 \<in> carrier R; a = h r1; r2 \<in> carrier R; b = h r2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ring_iso_def bij_betw_def
[PROOF STATE]
proof (prove)
using this:
a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)
b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)
h \<in> {h \<in> ring_hom R S. inj_on h (carrier R) \<and> h ` carrier R = carrier S}
(?z \<in> h ` carrier R) = (\<exists>x\<in>carrier R. ?z = h x)

goal (1 subgoal):
 1. (\<And>r1 r2. \<lbrakk>r1 \<in> carrier R; a = h r1; r2 \<in> carrier R; b = h r2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r1 \<in> carrier R
a = h r1
r2 \<in> carrier R
b = h r2

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
hence "a \<otimes>\<^bsub>?h_img\<^esub> b = h (r1 \<otimes> r2)"
[PROOF STATE]
proof (prove)
using this:
r1 \<in> carrier R
a = h r1
r2 \<in> carrier R
b = h r2

goal (1 subgoal):
 1. a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = h (r1 \<otimes> r2)
[PROOF STEP]
using assms r1 r2
[PROOF STATE]
proof (prove)
using this:
r1 \<in> carrier R
a = h r1
r2 \<in> carrier R
b = h r2
h \<in> ring_iso R S
r1 \<in> carrier R
a = h r1
r2 \<in> carrier R
b = h r2

goal (1 subgoal):
 1. a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = h (r1 \<otimes> r2)
[PROOF STEP]
unfolding ring_iso_def ring_hom_def
[PROOF STATE]
proof (prove)
using this:
r1 \<in> carrier R
a = h r1
r2 \<in> carrier R
b = h r2
h \<in> {h \<in> {h \<in> carrier R \<rightarrow> carrier S. (\<forall>x y. x \<in> carrier R \<and> y \<in> carrier R \<longrightarrow> h (x \<otimes> y) = h x \<otimes>\<^bsub>S\<^esub> h y \<and> h (x \<oplus> y) = h x \<oplus>\<^bsub>S\<^esub> h y) \<and> h \<one> = \<one>\<^bsub>S\<^esub>}. bij_betw h (carrier R) (carrier S)}
r1 \<in> carrier R
a = h r1
r2 \<in> carrier R
b = h r2

goal (1 subgoal):
 1. a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = h (r1 \<otimes> r2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = h (r1 \<otimes> r2)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
hence "h (r1 \<otimes> r2) = h \<zero>"
[PROOF STATE]
proof (prove)
using this:
a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = h (r1 \<otimes> r2)

goal (1 subgoal):
 1. h (r1 \<otimes> r2) = h \<zero>
[PROOF STEP]
using A(1)
[PROOF STATE]
proof (prove)
using this:
a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = h (r1 \<otimes> r2)
a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>

goal (1 subgoal):
 1. h (r1 \<otimes> r2) = h \<zero>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
h (r1 \<otimes> r2) = h \<zero>

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
hence "r1 \<otimes> r2 = \<zero>"
[PROOF STATE]
proof (prove)
using this:
h (r1 \<otimes> r2) = h \<zero>

goal (1 subgoal):
 1. r1 \<otimes> r2 = \<zero>
[PROOF STEP]
using ring_iso_memE(5)[OF assms] aux(1)[OF r1(1) r2(1)] aux(5)
[PROOF STATE]
proof (prove)
using this:
h (r1 \<otimes> r2) = h \<zero>
bij_betw h (carrier R) (carrier S)
r1 \<otimes> r2 \<in> carrier R
\<zero> \<in> carrier R

goal (1 subgoal):
 1. r1 \<otimes> r2 = \<zero>
[PROOF STEP]
unfolding bij_betw_def inj_on_def
[PROOF STATE]
proof (prove)
using this:
h (r1 \<otimes> r2) = h \<zero>
(\<forall>x\<in>carrier R. \<forall>y\<in>carrier R. h x = h y \<longrightarrow> x = y) \<and> h ` carrier R = carrier S
r1 \<otimes> r2 \<in> carrier R
\<zero> \<in> carrier R

goal (1 subgoal):
 1. r1 \<otimes> r2 = \<zero>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
r1 \<otimes> r2 = \<zero>

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
hence "r1 = \<zero> \<or> r2 = \<zero>"
[PROOF STATE]
proof (prove)
using this:
r1 \<otimes> r2 = \<zero>

goal (1 subgoal):
 1. r1 = \<zero> \<or> r2 = \<zero>
[PROOF STEP]
using aux(2)[OF _ r1(1) r2(1)]
[PROOF STATE]
proof (prove)
using this:
r1 \<otimes> r2 = \<zero>
r1 \<otimes> r2 = \<zero> \<Longrightarrow> r1 = \<zero> \<or> r2 = \<zero>

goal (1 subgoal):
 1. r1 = \<zero> \<or> r2 = \<zero>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r1 = \<zero> \<or> r2 = \<zero>

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<otimes>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>; a \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>); b \<in> carrier (S\<lparr>zero := h \<zero>\<rparr>)\<rbrakk> \<Longrightarrow> a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
thus "a = \<zero>\<^bsub>?h_img\<^esub> \<or> b = \<zero>\<^bsub>?h_img\<^esub>"
[PROOF STATE]
proof (prove)
using this:
r1 = \<zero> \<or> r2 = \<zero>

goal (1 subgoal):
 1. a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
unfolding r1 r2
[PROOF STATE]
proof (prove)
using this:
r1 = \<zero> \<or> r2 = \<zero>

goal (1 subgoal):
 1. h r1 = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> h r2 = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub> \<or> b = \<zero>\<^bsub>S\<lparr>zero := h \<zero>\<rparr>\<^esub>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
domain (S\<lparr>zero := h \<zero>\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed