---

Step * 1 1 1 of Lemma free_abmon_umap_properties_1


1. S : DSet
2. mon : AbMon
3. inj : |S| ⟶ |mon|
4. M2 : mon':AbMon ⟶ f':(|S| ⟶ |mon'|) ⟶ {!g:MonHom(mon,mon') | (g o inj) = f' ∈ (|S| ⟶ |mon'|)}
5. N : AbMon
6. p : |S| ⟶ |N|
7. M2 N p ∈ {!g:MonHom(mon,N) | (g o inj) = p ∈ (|S| ⟶ |N|)}
⊢ ((M2 N p) o inj) = p ∈ (|S| ⟶ |N|)
BY
{ ((MemTypeHD (-1)) THENA Auto) }

1
1. S : DSet
2. mon : AbMon
3. inj : |S| ⟶ |mon|
4. M2 : mon':AbMon ⟶ f':(|S| ⟶ |mon'|) ⟶ {!g:MonHom(mon,mon') | (g o inj) = f' ∈ (|S| ⟶ |mon'|)}
5. N : AbMon
6. p : |S| ⟶ |N|
7. (M2 N p) = (M2 N p) ∈ MonHom(mon,N)
8. (((M2 N p) o inj) = p ∈ (|S| ⟶ |N|))
∧ (∀y:MonHom(mon,N). (((y o inj) = p ∈ (|S| ⟶ |N|)) ⇒ (y = (M2 N p) ∈ MonHom(mon,N))))
⊢ ((M2 N p) o inj) = p ∈ (|S| ⟶ |N|)

---

Latex:

---

Latex:

1.  S  :  DSet
2.  mon  :  AbMon
3.  inj  :  |S|  {}\mrightarrow{}  |mon|
4.  M2  :  mon':AbMon  {}\mrightarrow{}  f':(|S|  {}\mrightarrow{}  |mon'|)  {}\mrightarrow{}  \{!g:MonHom(mon,mon')  |  (g  o  inj)  =  f'\}
5.  N  :  AbMon
6.  p  :  |S|  {}\mrightarrow{}  |N|
7.  M2  N  p  \mmember{}  \{!g:MonHom(mon,N)  |  (g  o  inj)  =  p\}
\mvdash{}  ((M2  N  p)  o  inj)  =  p


By

---

Latex:
((MemTypeHD  (-1))  THENA  Auto)

---

Home Index