set f = X --> 0 ;
A1: dom (X --> 0 ) = X by FUNCOP_1:19;
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 set such that
A2: x in support f by XBOOLE_0:def 1;
support f c= dom f by Th41;
then f . x = 0 by A1, A2, FUNCOP_1:13;
hence contradiction by A2, Def7; :: thesis: verum

end;

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