set f = X --> 0;
A1: dom (X --> 0) = X by FUNCOP_1:13;
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 Th37;
then f . x = 0 by A1, A2, FUNCOP_1:7;
hence contradiction by A2, Def7; :: thesis: verum

end;

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