let X be set ; :: thesis: for L being non empty ZeroStr
for s being Series of X,L
for Y being Subset of (Bags X) holds Support (s | Y) c= Support s
let L be non empty ZeroStr ; :: thesis: for s being Series of X,L
for Y being Subset of (Bags X) holds Support (s | Y) c= Support s
let s be Series of X,L; :: thesis: for Y being Subset of (Bags X) holds Support (s | Y) c= Support s
let Y be Subset of (Bags X); :: thesis: Support (s | Y) c= Support s
set m = ((Support s) \ Y) --> (0. L);
set r = s +* (((Support s) \ Y) --> (0. L));
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in Support (s | Y) or u in Support s )
assume A1: u in Support (s | Y) ; :: thesis: u in Support s
then reconsider u9 = u as Element of Bags X ;
A2: (s +* (((Support s) \ Y) --> (0. L))) . u9 <> 0. L by A1, POLYNOM1:def 4;

now :: thesis: ( ( u9 in dom (((Support s) \ Y) --> (0. L)) & u9 in Support s ) or ( not u9 in dom (((Support s) \ Y) --> (0. L)) & s . u9 <> 0. L ) )

per cases ( u9 in dom (((Support s) \ Y) --> (0. L)) or not u9 in dom (((Support s) \ Y) --> (0. L)) ) ;

case u9 in dom (((Support s) \ Y) --> (0. L)) ; :: thesis: u9 in Support s

hence u9 in Support s by XBOOLE_0:def 5; :: thesis: verum

end;

case not u9 in dom (((Support s) \ Y) --> (0. L)) ; :: thesis: s . u9 <> 0. L

hence s . u9 <> 0. L by A2, FUNCT_4:11; :: thesis: verum

end;

end;

end;

hence u in Support s by POLYNOM1:def 4; :: thesis: verum