take f = 0 .--> 1; :: thesis: ( f is natural-valued & f is finite-support & not f is empty )
thus f is natural-valued ; :: thesis: ( f is finite-support & not f is empty )
thus f is finite-support ; :: thesis: not f is empty
thus not f is empty ; :: thesis: verum