set Z = 0_ (n,S);

now

given x being set such that A1: x in Support (0_ (n,S)) ; :: thesis: contradiction
reconsider x = x as Element of Bags n by A1;
(0_ (n,S)) . x = 0. S by FUNCOP_1:7;
hence contradiction by A1, Def9; :: thesis: verum

end;

then Support (0_ (n,S)) = {} by XBOOLE_0:def 1;
hence 0_ (n,S) is finite-Support by Def10; :: thesis: verum