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

now

let x be set ; :: thesis: ( ( x in Support O' implies not x <> EmptyBag n ) & ( x = EmptyBag n implies x in Support O' ) )

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

assume A1: x in Support O' ; :: thesis: not x <> EmptyBag n
then reconsider x' = x as Element of Bags n ;
assume x <> EmptyBag n ; :: thesis: contradiction
then O' . x = (0_ n,L) . x' by FUNCT_7:34
.= 0. L by FUNCOP_1:13 ;
hence contradiction by A1, Def9; :: thesis: verum

end;

assume A2: x = EmptyBag n ; :: thesis: x in Support O'
dom (0_ n,L) = Bags n by FUNCOP_1:19;
then O' . x <> 0. L by A2, Th27, FUNCT_7:33;
hence x in Support O' by A2, Def9; :: thesis: verum

end;

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