reconsider O = (0_ (n,L)) +* ((EmptyBag n),(1. L)) as Function of (Bags n), the carrier of L ;
reconsider O9 = O as Function of (Bags n),L ;
reconsider O9 = O9 as Series of n,L ;

now :: thesis: for x being object holds
( ( x in Support O9 implies not x <> EmptyBag n ) & ( x = EmptyBag n implies x in Support O9 ) )

let x be object ; :: thesis: ( ( x in Support O9 implies not x <> EmptyBag n ) & ( x = EmptyBag n implies x in Support O9 ) )

hereby :: thesis: ( x = EmptyBag n implies x in Support O9 )

assume A1: x in Support O9 ; :: thesis: not x <> EmptyBag n
then reconsider x9 = x as Element of Bags n ;
assume x <> EmptyBag n ; :: thesis: contradiction
then O9 . x = (0_ (n,L)) . x9 by FUNCT_7:32
.= 0. L ;
hence contradiction by A1, Def4; :: thesis: verum

end;

assume A2: x = EmptyBag n ; :: thesis: x in Support O9
dom (0_ (n,L)) = Bags n ;
then O9 . x <> 0. L by A2, FUNCT_7:31;
hence x in Support O9 by A2, Def4; :: thesis: verum

end;

then Support O9 = {(EmptyBag n)} by TARSKI:def 1;
hence 1_ (n,L) is finite-Support ; :: thesis: verum