[STATEMENT]
lemma (in Group) nsg2:"\<lbrakk>G \<guillemotright> H; b \<in> carrier G; h \<in> H;  
       \<forall>a\<in>carrier G. \<forall>h\<in>H. (a \<cdot> h) \<cdot> (\<rho> a) \<in> H\<rbrakk> \<Longrightarrow>  (\<rho> b) \<cdot> h \<cdot> b \<in> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G \<guillemotright> H ; b \<in> carrier G; h \<in> H; \<forall>a\<in>carrier G. \<forall>h\<in>H. a \<cdot> h \<cdot> \<rho> a \<in> H\<rbrakk> \<Longrightarrow> \<rho> b \<cdot> h \<cdot> b \<in> H
[PROOF STEP]
apply (frule i_closed[of "b"], 
       frule_tac x = "\<rho> b" in bspec, assumption,
       thin_tac "\<forall>a\<in>carrier G. \<forall>h\<in>H. a \<cdot> h \<cdot> \<rho> a \<in> H",
       frule_tac x = h in bspec, assumption,
       thin_tac "\<forall>h\<in>H. \<rho> b \<cdot> h \<cdot> \<rho> (\<rho> b) \<in> H")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G \<guillemotright> H ; b \<in> carrier G; h \<in> H; \<rho> b \<in> carrier G; \<rho> b \<cdot> h \<cdot> \<rho> (\<rho> b) \<in> H\<rbrakk> \<Longrightarrow> \<rho> b \<cdot> h \<cdot> b \<in> H
[PROOF STEP]
apply (simp add:iop_i_i)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done