---

Step * 1 of Lemma funinv-ap-equals

.....assertion..... 
1. n : ℕ
2. f : ℕn →⟶ ℕn
3. a : ℕn
4. b : ℕn
5. (f a) = b ∈ ℤ
6. inv(f) ∈ ℕn →⟶ ℕn
7. (f a) = b ∈ {z:ℤ| (z = (f a) ∈ ℤ) ∧ (z = b ∈ ℤ)} 
8. (inv(f) (f a)) = (inv(f) b) ∈ ℤ
⊢ (inv(f) (f a)) = a ∈ ℤ
BY
{ (BLemma `funinv-property` THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  n  :  \mBbbN{}
2.  f  :  \mBbbN{}n  \mrightarrow{}{}\mrightarrow{}  \mBbbN{}n
3.  a  :  \mBbbN{}n
4.  b  :  \mBbbN{}n
5.  (f  a)  =  b
6.  inv(f)  \mmember{}  \mBbbN{}n  \mrightarrow{}{}\mrightarrow{}  \mBbbN{}n
7.  (f  a)  =  b
8.  (inv(f)  (f  a))  =  (inv(f)  b)
\mvdash{}  (inv(f)  (f  a))  =  a


By

---

Latex:
(BLemma  `funinv-property`  THEN  Auto)

---

Home Index