equal
deleted
inserted
replaced
1653 and ascarr: "set fa \<subseteq> carrier G" and bscarr:"set fb \<subseteq> carrier G" |
1653 and ascarr: "set fa \<subseteq> carrier G" and bscarr:"set fb \<subseteq> carrier G" |
1654 shows "factors G (fa @ fb) (a \<otimes> b)" |
1654 shows "factors G (fa @ fb) (a \<otimes> b)" |
1655 using assms |
1655 using assms |
1656 unfolding factors_def |
1656 unfolding factors_def |
1657 apply (safe, force) |
1657 apply (safe, force) |
|
1658 apply hypsubst_thin |
1658 apply (induct fa) |
1659 apply (induct fa) |
1659 apply simp |
1660 apply simp |
1660 apply (simp add: m_assoc) |
1661 apply (simp add: m_assoc) |
1661 done |
1662 done |
1662 |
1663 |