---

Step * 1 1 1 of Lemma zero_sym_grp


1. f : ℕ0 ⟶ ℕ0@i
2. p1 : ℕ0 ⟶ ℕ0@i
3. InvFuns(ℕ0;ℕ0;<f, p1>.f;<f, p1>.b)
⊢ <f, p1> = <Id, Id> ∈ (f:ℕ0 ⟶ ℕ0 × (ℕ0 ⟶ ℕ0))
BY
{ ((EqCD THENA Auto) THEN ExtWith [] [ℕ0 ⟶ ℕ0] THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  \mBbbN{}0  {}\mrightarrow{}  \mBbbN{}0@i
2.  p1  :  \mBbbN{}0  {}\mrightarrow{}  \mBbbN{}0@i
3.  InvFuns(\mBbbN{}0;\mBbbN{}0;<f,  p1>.f;<f,  p1>.b)
\mvdash{}  <f,  p1>  =  <Id,  Id>


By

---

Latex:
((EqCD  THENA  Auto)  THEN  ExtWith  []  [\mBbbN{}0  {}\mrightarrow{}  \mBbbN{}0]  THEN  Auto)

---

Home Index