set f = X --> 0;
reconsider f = X --> 0 as ManySortedSet of X ;
take f ; :: thesis: ( f is natural-valued & f is finite-support )
thus f is natural-valued ; :: thesis: f is finite-support
support f = {}

proof

assume not support f = {} ; :: thesis: contradiction
then consider x being object such that
A2: x in support f by XBOOLE_0:def 1;
f . x = 0 ;
hence contradiction by A2, Def7; :: thesis: verum

end;

hence f is finite-support ; :: thesis: verum