set V = { x where x is Element of X : ex b being bag of X st
( b in Support p & b . x <> 0 ) } ;
{ x where x is Element of X : ex b being bag of X st
( b in Support p & b . x <> 0 ) } c= X

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of X : ex b being bag of X st
( b in Support p & b . x <> 0 ) } or y in X )
assume y in { x where x is Element of X : ex b being bag of X st
( b in Support p & b . x <> 0 ) } ; :: thesis: y in X
then consider x being Element of X such that
A1: ( x = y & ex b being bag of X st
( b in Support p & b . x <> 0 ) ) ;
consider b being bag of X such that
A2: ( b in Support p & b . x <> 0 ) by A1;
( x in dom b & dom b = X ) by A2, FUNCT_1:def 2, PARTFUN1:def 2;
hence y in X by A1; :: thesis: verum

end;

then reconsider V = { x where x is Element of X : ex b being bag of X st
( b in Support p & b . x <> 0 ) } as Subset of X ;
take V ; :: thesis: for x being object holds
( x in V iff ex b being bag of X st
( b in Support p & b . x <> 0 ) )
let y be object ; :: thesis: ( y in V iff ex b being bag of X st
( b in Support p & b . y <> 0 ) )
thus ( y in V implies ex b being bag of X st
( b in Support p & b . y <> 0 ) ) :: thesis: ( ex b being bag of X st
( b in Support p & b . y <> 0 ) implies y in V )

proof

assume y in V ; :: thesis: ex b being bag of X st
( b in Support p & b . y <> 0 )
then ex x being Element of X st
( y = x & ex b being bag of X st
( b in Support p & b . x <> 0 ) ) ;
hence ex b being bag of X st
( b in Support p & b . y <> 0 ) ; :: thesis: verum

end;

given b being bag of X such that A3: ( b in Support p & b . y <> 0 ) ; :: thesis: y in V
( y in dom b & dom b = X ) by A3, FUNCT_1:def 2, PARTFUN1:def 2;
hence y in V by A3; :: thesis: verum