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 set ; :: according to TARSKI:def 3 :: thesis: ( not u in Support (s | Y) or u in Support s )
assume A2: u in Support (s | Y) ; :: thesis: u in Support s
then reconsider u' = u as Element of Bags X ;
A3: (s +* (((Support s) \ Y) --> (0. L))) . u' <> 0. L by A2, POLYNOM1:def 9;

now

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

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

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

end;

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

hence s . u' <> 0. L by A3, FUNCT_4:12; :: thesis: verum

end;

end;

end;

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