Theorem measvxrge0

Description: The values of a measure are positive extended reals. (Contributed by Thierry Arnoux, 26-Dec-2016)

	Ref	Expression
Assertion	measvxrge0	|- ( ( M e. ( measures ` S ) /\ A e. S ) -> ( M ` A ) e. ( 0 [,] +oo ) )

Proof

Step	Hyp	Ref	Expression
1		measfrge0	|- ( M e. ( measures ` S ) -> M : S --> ( 0 [,] +oo ) )
2	1	ffvelcdmda	|- ( ( M e. ( measures ` S ) /\ A e. S ) -> ( M ` A ) e. ( 0 [,] +oo ) )