---

Step * 1 1 of Lemma grp_op_ap2_functionality_wrt_massoc


1. g : IAbMonoid@i'
2. a : |g|@i
3. a' : |g|@i
4. b : |g|@i
5. b' : |g|@i
6. a | b@i
7. b | a@i
8. a' | b'@i
9. b' | a'@i
⊢ (a * a') | (b * b')
BY
{ ((BLemma `grp_op_ap2_functionality_wrt_mdivides`) THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  IAbMonoid@i'
2.  a  :  |g|@i
3.  a'  :  |g|@i
4.  b  :  |g|@i
5.  b'  :  |g|@i
6.  a  |  b@i
7.  b  |  a@i
8.  a'  |  b'@i
9.  b'  |  a'@i
\mvdash{}  (a  *  a')  |  (b  *  b')


By

---

Latex:
((BLemma  `grp\_op\_ap2\_functionality\_wrt\_mdivides`)  THEN  Auto)

---

Home Index