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);
set e = s | ({} (Bags X));
( s | (Support s) = s +* ({} --> (0. L)) & dom ({} --> (0. L)) = {} ) by XBOOLE_1:37;
hence s | (Support s) = s +* {}
.= s ;
:: thesis: s | ({} (Bags X)) = 0_ (X,L)
A1: dom ((Support s) --> (0. L)) = Support s by FUNCOP_1:13;
A2: now :: thesis: for u being object st u in dom (s | ({} (Bags X))) holds
(s | ({} (Bags X))) . u = (0_ (X,L)) . u
let u be object ; :: 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 u9 = u as Element of Bags X ;
now :: thesis: ( ( u9 in Support s & (s | ({} (Bags X))) . u9 = (0_ (X,L)) . u9 ) or ( not u9 in Support s & (s | ({} (Bags X))) . u9 = (0_ (X,L)) . u9 ) )
per cases ( u9 in Support s or not u9 in Support s ) ;
case A3: u9 in Support s ; :: thesis: (s | ({} (Bags X))) . u9 = (0_ (X,L)) . u9
then (s | ({} (Bags X))) . u9 = ((Support s) --> (0. L)) . u9 by A1, FUNCT_4:13
.= 0. L by A3, FUNCOP_1:7 ;
hence (s | ({} (Bags X))) . u9 = (0_ (X,L)) . u9 by POLYNOM1:22; :: thesis: verum
end;
case A4: not u9 in Support s ; :: thesis: (s | ({} (Bags X))) . u9 = (0_ (X,L)) . u9
then (s | ({} (Bags X))) . u9 = s . u9 by A1, FUNCT_4:11;
then (s | ({} (Bags X))) . u9 = 0. L by A4, POLYNOM1:def 4;
hence (s | ({} (Bags X))) . u9 = (0_ (X,L)) . u9 by POLYNOM1:22; :: thesis: verum
end;
end;
end;
hence (s | ({} (Bags X))) . u = (0_ (X,L)) . u ; :: thesis: verum
end;
dom (s | ({} (Bags X))) = Bags X by FUNCT_2:def 1
.= dom (0_ (X,L)) by FUNCT_2:def 1 ;
hence s | ({} (Bags X)) = 0_ (X,L) by A2, FUNCT_1:2; :: thesis: verum