let X be set ; :: thesis: for L being non empty ZeroStr
for s being Series of X,L holds
( s | (Support s) = s & s | ({} (Bags X)) = 0_ X,L )
let L be non empty ZeroStr ; :: thesis: for s being Series of X,L holds
( s | (Support s) = s & s | ({} (Bags X)) = 0_ X,L )
let s be Series of X,L; :: thesis: ( s | (Support s) = s & s | ({} (Bags X)) = 0_ X,L )
set r = s | (Support s);
A1: s | (Support s) = s +* ({} --> (0. L)) by XBOOLE_1:37;
dom ({} --> (0. L)) = {} ;
hence s | (Support s) = s +* {} by A1, RELAT_1:64
.= s by FUNCT_4:22 ;
:: thesis: s | ({} (Bags X)) = 0_ X,L
set e = s | ({} (Bags X));
A2: dom ((Support s) --> (0. L)) = Support s by FUNCOP_1:19;
A3: dom (s | ({} (Bags X))) = Bags X by FUNCT_2:def 1
.= dom (0_ X,L) by FUNCT_2:def 1 ;

now

let u be set ; :: thesis: ( u in dom (s | ({} (Bags X))) implies (s | ({} (Bags X))) . u = (0_ X,L) . u )
assume u in dom (s | ({} (Bags X))) ; :: thesis: (s | ({} (Bags X))) . u = (0_ X,L) . u
then reconsider u' = u as Element of Bags X ;

now

per cases ( u' in Support s or not u' in Support s ) ;

case A4: u' in Support s ; :: thesis: (s | ({} (Bags X))) . u' = (0_ X,L) . u'

then (s | ({} (Bags X))) . u' = ((Support s) --> (0. L)) . u' by A2, FUNCT_4:14
.= 0. L by A4, FUNCOP_1:13 ;
hence (s | ({} (Bags X))) . u' = (0_ X,L) . u' by POLYNOM1:81; :: thesis: verum

end;

case A5: not u' in Support s ; :: thesis: (s | ({} (Bags X))) . u' = (0_ X,L) . u'

then (s | ({} (Bags X))) . u' = s . u' by A2, FUNCT_4:12;
then (s | ({} (Bags X))) . u' = 0. L by A5, POLYNOM1:def 9;
hence (s | ({} (Bags X))) . u' = (0_ X,L) . u' by POLYNOM1:81; :: thesis: verum

end;

end;

end;

hence (s | ({} (Bags X))) . u = (0_ X,L) . u ; :: thesis: verum

end;

hence s | ({} (Bags X)) = 0_ X,L by A3, FUNCT_1:9; :: thesis: verum