[STATEMENT]
lemma (in group) IDirProds_subgroup_id: "subgroup (S i) G \<Longrightarrow> IDirProds G S {i} = S i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgroup (S i) G \<Longrightarrow> IDirProds G S {i} = S i
[PROOF STEP]
by (simp add: generate_subgroup_id IDirProds_def)