let R be non degenerated comRing; :: thesis: for f being Series of 1,R holds BagN1 .: (Support f) = Support (f * NBag1)
let f be Series of 1,R; :: thesis: BagN1 .: (Support f) = Support (f * NBag1)
for o being object holds
( o in BagN1 .: (Support f) iff o in Support (f * NBag1) )

proof

let o be object ; :: thesis: ( o in BagN1 .: (Support f) iff o in Support (f * NBag1) )
A1: dom BagN1 = Bags 1 by FUNCT_2:def 1;
A2: dom (f * NBag1) = NAT by FUNCT_2:def 1;
A3: ( o in BagN1 .: (Support f) implies o in Support (f * NBag1) )

proof

assume o in BagN1 .: (Support f) ; :: thesis: o in Support (f * NBag1)
then consider x being object such that
A4: ( x in dom BagN1 & x in Support f & o = BagN1 . x ) by FUNCT_1:def 6;
A5: o in NAT by A4, FUNCT_2:5;
(f * NBag1) . o = ((f * NBag1) * BagN1) . x by A4, FUNCT_2:15
.= f . x by Th38 ;
then (f * NBag1) . o <> 0. R by A4, POLYNOM1:def 3;
hence o in Support (f * NBag1) by A5, A2, POLYNOM1:def 3; :: thesis: verum

end;

( o in Support (f * NBag1) implies o in BagN1 .: (Support f) )

proof

assume A6: o in Support (f * NBag1) ; :: thesis: o in BagN1 .: (Support f)
then reconsider b = NBag1 . o as Element of Bags 1 by FUNCT_2:5;
A7: dom f = Bags 1 by FUNCT_2:def 1;
A8: BagN1 . b = (id NAT) . o by A6, FUNCT_2:15, Th10
.= o by A6, FUNCT_1:18 ;
f . b = (f * NBag1) . o by A6, FUNCT_2:15;
then f . b <> 0. R by A6, POLYNOM1:def 3;
then b in Support f by A7, POLYNOM1:def 3;
hence o in BagN1 .: (Support f) by A1, A8, FUNCT_1:def 6; :: thesis: verum

end;

hence ( o in BagN1 .: (Support f) iff o in Support (f * NBag1) ) by A3; :: thesis: verum

end;

hence BagN1 .: (Support f) = Support (f * NBag1) by TARSKI:2; :: thesis: verum