set f = X --> 0;
reconsider f = X --> 0 as Function of X,NAT ;
take f ; :: thesis: f is finite-support
now :: thesis: not support f <> {}
assume support f <> {} ; :: thesis: contradiction
then consider x being object such that
A3: x in support f by XBOOLE_0:def 1;
f . x <> 0 by A3, Def7;
hence contradiction ; :: thesis: verum
end;
hence support f is finite ; :: according to PRE_POLY:def 8 :: thesis: verum