Theorem fsuppfund

Description: A finitely supported function is a function. (Contributed by SN, 8-Mar-2025)

	Ref	Expression
Hypothesis	fsuppfund.1	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )
Assertion	fsuppfund	⊢ ( 𝜑 → Fun 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		fsuppfund.1	⊢ ( 𝜑 → 𝐹 finSupp 𝑍 )
2		fsuppimp	⊢ ( 𝐹 finSupp 𝑍 → ( Fun 𝐹 ∧ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
3	2	simpld	⊢ ( 𝐹 finSupp 𝑍 → Fun 𝐹 )
4	1 3	syl	⊢ ( 𝜑 → Fun 𝐹 )