Theorem measfn

Description: A measure is a function on its base sigma-algebra. (Contributed by Thierry Arnoux, 13-Feb-2017)

	Ref	Expression
Assertion	measfn	⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑀 Fn 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		measfrge0	⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )
2	1	ffnd	⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑀 Fn 𝑆 )