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) = (Support s) /\ Y & ( for b being bag of X st b in Support (s | Y) holds
(s | Y) . b = s . b ) )
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) = (Support s) /\ Y & ( for b being bag of X st b in Support (s | Y) holds
(s | Y) . b = s . b ) )
let s be Series of X,L; :: thesis: for Y being Subset of (Bags X) holds
( Support (s | Y) = (Support s) /\ Y & ( for b being bag of X st b in Support (s | Y) holds
(s | Y) . b = s . b ) )
let Y be Subset of (Bags X); :: thesis: ( Support (s | Y) = (Support s) /\ Y & ( for b being bag of X st b in Support (s | Y) holds
(s | Y) . b = s . b ) )
set m = ((Support s) \ Y) --> (0. L);
set r = s +* (((Support s) \ Y) --> (0. L));

A1: now

let u be set ; :: thesis: ( u in Support (s | Y) implies u in (Support s) /\ Y )
assume A2: u in Support (s | Y) ; :: thesis: u in (Support s) /\ Y
then reconsider u9 = u as Element of Bags X ;

A3: now

assume A4: u9 in dom (((Support s) \ Y) --> (0. L)) ; :: thesis: contradiction
then (s +* (((Support s) \ Y) --> (0. L))) . u9 = (((Support s) \ Y) --> (0. L)) . u9 by FUNCT_4:14
.= 0. L by A4, FUNCOP_1:13 ;
hence contradiction by A2, POLYNOM1:def 9; :: thesis: verum

end;

(s +* (((Support s) \ Y) --> (0. L))) . u9 <> 0. L by A2, POLYNOM1:def 9;
then s . u9 <> 0. L by A3, FUNCT_4:12;
then A5: u9 in Support s by POLYNOM1:def 9;
dom (((Support s) \ Y) --> (0. L)) = (Support s) \ Y by FUNCOP_1:19;
then u9 in Y by A3, A5, XBOOLE_0:def 5;
hence u in (Support s) /\ Y by A5, XBOOLE_0:def 4; :: thesis: verum

end;

A6: dom (((Support s) \ Y) --> (0. L)) = (Support s) \ Y by FUNCOP_1:19;

now

let u be set ; :: thesis: ( u in (Support s) /\ Y implies u in Support (s | Y) )
assume A7: u in (Support s) /\ Y ; :: thesis: u in Support (s | Y)
then A8: u in Support s by XBOOLE_0:def 4;
then reconsider u9 = u as Element of Bags X ;
u in Y by A7, XBOOLE_0:def 4;
then not u in (Support s) \ Y by XBOOLE_0:def 5;
then (s +* (((Support s) \ Y) --> (0. L))) . u9 = s . u9 by A6, FUNCT_4:12;
then (s +* (((Support s) \ Y) --> (0. L))) . u9 <> 0. L by A8, POLYNOM1:def 9;
hence u in Support (s | Y) by POLYNOM1:def 9; :: thesis: verum

end;

hence A9: Support (s | Y) = (Support s) /\ Y by A1, TARSKI:2; :: thesis: for b being bag of X st b in Support (s | Y) holds
(s | Y) . b = s . b

now

let b be bag of X; :: thesis: ( b in Support (s | Y) implies (s | Y) . b = s . b )
assume b in Support (s | Y) ; :: thesis: (s | Y) . b = s . b
then b in Y by A9, XBOOLE_0:def 4;
then not b in dom (((Support s) \ Y) --> (0. L)) by XBOOLE_0:def 5;
hence (s | Y) . b = s . b by FUNCT_4:12; :: thesis: verum

end;

hence for b being bag of X st b in Support (s | Y) holds
(s | Y) . b = s . b ; :: thesis: verum