---

Step * 2 of Lemma cdrng_is_abdgrp

.....set predicate..... 
1. r : CRng
2. IsEqFun(|r|;=b)
⊢ IsEqFun(|r↓+gp|;=b)
BY
{ (NthHypSq (-1) ⋅ THEN EqCD THEN Computation) }

---

Latex:

---

Latex:
.....set  predicate..... 
1.  r  :  CRng
2.  IsEqFun(|r|;=\msubb{})
\mvdash{}  IsEqFun(|r\mdownarrow{}+gp|;=\msubb{})


By

---

Latex:
(NthHypSq  (-1)  \mcdot{}  THEN  EqCD  THEN  Computation)

---

Home Index