set Z = 0_ (n,S);

now :: thesis: for x being object holds not x in Support (0_ (n,S))

given x being object 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 ;
hence contradiction by A1, Def4; :: thesis: verum

end;

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