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 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 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 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 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: dom (((Support s) \ Y) --> (0. L)) = (Support s) \ Y by FUNCOP_1:19;

A2: now

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

end;

now

let u be set ; :: thesis: ( u in Support (s | Y) implies u in (Support s) /\ Y )
assume A4: u in Support (s | Y) ; :: thesis: u in (Support s) /\ Y
then reconsider u' = u as Element of Bags X ;
A5: (s +* (((Support s) \ Y) --> (0. L))) . u' <> 0. L by A4, POLYNOM1:def 9;
A6: dom (((Support s) \ Y) --> (0. L)) = (Support s) \ Y by FUNCOP_1:19;

A7: now

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

end;

then s . u' <> 0. L by A5, FUNCT_4:12;
then A9: u' in Support s by POLYNOM1:def 9;
then u' in Y by A6, A7, XBOOLE_0:def 5;
hence u in (Support s) /\ Y by A9, XBOOLE_0:def 4; :: thesis: verum

end;

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

now

let b be bag of ; :: 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 Support s & b in Y ) by A10, 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 st b in Support (s | Y) holds
(s | Y) . b = s . b ; :: thesis: verum