let n be Nat; :: thesis: for b being bag of n holds support b = support (b bag_extend 0)
let b be bag of n; :: thesis: support b = support (b bag_extend 0)
set E = b bag_extend 0;
A1: b = (b bag_extend 0) | n by HILBASIS:def 1;
thus support b c= support (b bag_extend 0) :: according to XBOOLE_0:def 10 :: thesis: support (b bag_extend 0) c= support b

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support b or x in support (b bag_extend 0) )
assume x in support b ; :: thesis: x in support (b bag_extend 0)
then A2: b . x <> 0 by PRE_POLY:def 7;
then x in dom b by FUNCT_1:def 2;
then (b bag_extend 0) . x = b . x by A1, FUNCT_1:49;
hence x in support (b bag_extend 0) by A2, PRE_POLY:def 7; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (b bag_extend 0) or x in support b )
assume x in support (b bag_extend 0) ; :: thesis: x in support b
then A3: (b bag_extend 0) . x <> 0 by PRE_POLY:def 7;
then A4: ( x <> n & x in dom (b bag_extend 0) ) by HILBASIS:def 1, FUNCT_1:def 2;
dom (b bag_extend 0) = Segm (n + 1) by PARTFUN1:def 2;
then x in (Segm n) \/ {n} by A4, AFINSQ_1:2;
then (b bag_extend 0) . x = b . x by A1, FUNCT_1:49, A4, ZFMISC_1:136;
hence x in support b by A3, PRE_POLY:def 7; :: thesis: verum