---

Step * 1 of Lemma grp_op_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. a' ~ b'@i
⊢ (a * a') ~ (b * b')
BY
{ OnCls [0;6;7] (RepUnfolds ``massoc symmetrize``) 
THEN OnMCls [7;6] ExistHD THEN D 0 }

1
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')

2
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
⊢ (b * b') | (a * a')

---

Latex:

---

Latex:

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


By

---

Latex:
OnCls  [0;6;7]  (RepUnfolds  ``massoc  symmetrize``) 
THEN  OnMCls  [7;6]  ExistHD  THEN  D  0

---

Home Index