Theorem cofuterm

Description: Post-compose with a functor to a terminal category. (Contributed by Zhi Wang, 17-Nov-2025)

	Ref	Expression
Hypotheses	cofuterm.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	cofuterm.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
	cofuterm.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐶 Func 𝐸 ) )
	cofuterm.e	⊢ ( 𝜑 → 𝐸 ∈ TermCat )
Assertion	cofuterm	⊢ ( 𝜑 → ( 𝐺 ∘func 𝐹 ) = 𝐾 )

Proof

Step	Hyp	Ref	Expression
1		cofuterm.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
2		cofuterm.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐷 Func 𝐸 ) )
3		cofuterm.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐶 Func 𝐸 ) )
4		cofuterm.e	⊢ ( 𝜑 → 𝐸 ∈ TermCat )
5		eqid	⊢ ( 𝐶 FuncCat 𝐸 ) = ( 𝐶 FuncCat 𝐸 )
6	1	func1st2nd	⊢ ( 𝜑 → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
7	6	funcrcl2	⊢ ( 𝜑 → 𝐶 ∈ Cat )
8	5 7 4	fucterm	⊢ ( 𝜑 → ( 𝐶 FuncCat 𝐸 ) ∈ TermCat )
9	5	fucbas	⊢ ( 𝐶 Func 𝐸 ) = ( Base ‘ ( 𝐶 FuncCat 𝐸 ) )
10	1 2	cofucl	⊢ ( 𝜑 → ( 𝐺 ∘func 𝐹 ) ∈ ( 𝐶 Func 𝐸 ) )
11	8 9 10 3	termcbasmo	⊢ ( 𝜑 → ( 𝐺 ∘func 𝐹 ) = 𝐾 )