set f = X --> 0 ;
A1: dom (X --> 0 ) = X by FUNCOP_1:19;
reconsider f = X --> 0 as Function of X,NAT ;
take f ; :: thesis: f is finite-support

now

assume support f <> {} ; :: thesis: contradiction
then consider x being set such that
A3: x in support f by XBOOLE_0:def 1;
A4: f . x <> 0 by A3, Def7;
support f c= dom f by Th41;
hence contradiction by A1, A3, A4, FUNCOP_1:13; :: thesis: verum

end;

hence support f is finite ; :: according to POLYNOM1:def 8 :: thesis: verum