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

now

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

end;

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