let V1, V2 be Subset of X; :: thesis: ( ( for x being object holds
( x in V1 iff ex b being bag of X st
( b in Support p & b . x <> 0 ) ) ) & ( for x being object holds
( x in V2 iff ex b being bag of X st
( b in Support p & b . x <> 0 ) ) ) implies V1 = V2 )
assume that
A4: for x being object holds
( x in V1 iff ex b being bag of X st
( b in Support p & b . x <> 0 ) ) and
A5: for x being object holds
( x in V2 iff ex b being bag of X st
( b in Support p & b . x <> 0 ) ) ; :: thesis: V1 = V2

now :: thesis: for y being object holds
( y in V1 iff y in V2 )

let y be object ; :: thesis: ( y in V1 iff y in V2 )
( y in V1 iff ex b being bag of X st
( b in Support p & b . y <> 0 ) ) by A4;
hence ( y in V1 iff y in V2 ) by A5; :: thesis: verum

end;

hence V1 = V2 by TARSKI:2; :: thesis: verum