set m = ((Support s) \ Y) --> (0. L);
set r = s +* (((Support s) \ Y) --> (0. L));
A1: dom s = Bags X by FUNCT_2:def 1;
A2: dom (((Support s) \ Y) --> (0. L)) = (Support s) \ Y by FUNCOP_1:19;
then A3: dom (s +* (((Support s) \ Y) --> (0. L))) = (Bags X) \/ ((Support s) \ Y) by A1, FUNCT_4:def 1;

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 (Support s) \ Y c= Bags X by TARSKI:def 3;
then A4: dom (s +* (((Support s) \ Y) --> (0. L))) = Bags X by A3, XBOOLE_1:12;

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 A5: 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, A5, 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;

hence s +* (((Support s) \ Y) --> (0. L)) is Series of X,L by A4, FUNCT_2:5; :: thesis: verum