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

proof

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

proof

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

end;

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

proof

assume A6: o in Support (f * BagN1) ; :: thesis: o in NBag1 .: (Support f)
then reconsider b = BagN1 . o as Element of NAT by FUNCT_2:5;
A7: dom f = NAT by FUNCT_2:def 1;
A8: NBag1 . b = (id (Bags 1)) . o by A6, FUNCT_2:15, Th11
.= o by A6, FUNCT_1:18 ;
f . b = (f * BagN1) . 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 NBag1 .: (Support f) by A1, A8, FUNCT_1:def 6; :: thesis: verum

end;

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

end;

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