[STATEMENT]
lemma power_set_Suc2:
  "A *^ (Suc n) = A *^ n ** A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *^ Suc n = A *^ n ** A
[PROOF STEP]
apply (induct_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. A *^ Suc 0 = A *^ 0 ** A
 2. \<And>n. A *^ Suc n = A *^ n ** A \<Longrightarrow> A *^ Suc (Suc n) = A *^ Suc n ** A
[PROOF STEP]
apply (simp add: times_set_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. A *^ Suc n = A *^ n ** A \<Longrightarrow> A *^ Suc (Suc n) = A *^ Suc n ** A
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. A ** A *^ n = A *^ n ** A \<Longrightarrow> A ** (A *^ n ** A) = A *^ n ** A ** A
[PROOF STEP]
apply (subst times_set_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. A ** A *^ n = A *^ n ** A \<Longrightarrow> A ** A *^ n ** A = A *^ n ** A ** A
[PROOF STEP]
by simp