Step
*
2
of Lemma
group-cat_wf
.....set predicate.....
1. G : Group{i}
2. H : Group{i}
3. z : Group{i}
4. K : Group{i}
5. f : |G| ⟶ |H|
6. IsMonHom{G,H}(f)
7. g : MonHom(H,z)
8. h : MonHom(z,K)
⊢ IsMonHom{G,K}((h o g) o f)
BY
{ ((DVar `g' THENA Auto) THEN (DVar `h' THENA Auto) THEN All (RepUR ``monoid_hom_p fun_thru_2op``) THEN Auto) }
Latex:
Latex:
.....set predicate.....
1. G : Group\{i\}
2. H : Group\{i\}
3. z : Group\{i\}
4. K : Group\{i\}
5. f : |G| {}\mrightarrow{} |H|
6. IsMonHom\{G,H\}(f)
7. g : MonHom(H,z)
8. h : MonHom(z,K)
\mvdash{} IsMonHom\{G,K\}((h o g) o f)
By
Latex:
((DVar `g' THENA Auto)
THEN (DVar `h' THENA Auto)
THEN All (RepUR ``monoid\_hom\_p fun\_thru\_2op``)
THEN Auto)
Home
Index