set m = ((Support s) \ Y) --> (0. L);
set r = s +* (((Support s) \ Y) --> (0. L));

A1: now

let x be set ; :: thesis: ( x in Bags X implies (s +* (((Support s) \ Y) --> (0. L))) . x in the carrier of L )
assume x in Bags X ; :: thesis: (s +* (((Support s) \ Y) --> (0. L))) . x in the carrier of L
then reconsider x' = x as Element of Bags X ;

now

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

case A2: x' in dom (((Support s) \ Y) --> (0. L)) ; :: thesis: (s +* (((Support s) \ Y) --> (0. L))) . x in the carrier of L

then (s +* (((Support s) \ Y) --> (0. L))) . x' = (((Support s) \ Y) --> (0. L)) . x' by FUNCT_4:14
.= 0. L by A2, FUNCOP_1:13 ;
hence (s +* (((Support s) \ Y) --> (0. L))) . x in the carrier of L ; :: thesis: verum

end;

case not x in dom (((Support s) \ Y) --> (0. L)) ; :: thesis: (s +* (((Support s) \ Y) --> (0. L))) . x in the carrier of L

then (s +* (((Support s) \ Y) --> (0. L))) . x' = s . x' by FUNCT_4:12;
hence (s +* (((Support s) \ Y) --> (0. L))) . x in the carrier of L ; :: thesis: verum

end;

end;

end;

hence (s +* (((Support s) \ Y) --> (0. L))) . x in the carrier of L ; :: thesis: verum

end;

now

let u be set ; :: thesis: ( u in (Support s) \ Y implies u in Bags X )
assume u in (Support s) \ Y ; :: thesis: u in Bags X
then u in Support s by XBOOLE_0:def 5;
hence u in Bags X ; :: thesis: verum

end;

then A3: (Support s) \ Y c= Bags X by TARSKI:def 3;
( dom s = Bags X & dom (((Support s) \ Y) --> (0. L)) = (Support s) \ Y ) by FUNCOP_1:19, FUNCT_2:def 1;
then dom (s +* (((Support s) \ Y) --> (0. L))) = (Bags X) \/ ((Support s) \ Y) by FUNCT_4:def 1;
hence s +* (((Support s) \ Y) --> (0. L)) is Series of X,L by A3, A1, FUNCT_2:5, XBOOLE_1:12; :: thesis: verum