---

Step * 1 of Lemma grp_op_l


1. g : GrpSig
2. a : |g|
3. b : |g|
4. c : |g|
5. b = c ∈ |g|
⊢ (a * b) = (a * c) ∈ |g|
BY
{ HypSubst 5 0 THEN Auto }

---

Latex:

---

Latex:

1.  g  :  GrpSig
2.  a  :  |g|
3.  b  :  |g|
4.  c  :  |g|
5.  b  =  c
\mvdash{}  (a  *  b)  =  (a  *  c)


By

---

Latex:
HypSubst  5  0  THEN  Auto

---

Home Index