let D1, D2 be set ; :: thesis: ( ( for x being set holds
( x in D1 iff x is Linear_Combination of V ) ) & ( for x being set holds
( x in D2 iff x is Linear_Combination of V ) ) implies D1 = D2 )

assume A2: for x being set holds
( x in D1 iff x is Linear_Combination of V ) ; :: thesis: ( ex x being set st
( ( x in D2 implies x is Linear_Combination of V ) implies ( x is Linear_Combination of V & not x in D2 ) ) or D1 = D2 )

assume A3: for x being set holds
( x in D2 iff x is Linear_Combination of V ) ; :: thesis: D1 = D2
thus D1 c= D2 :: according to XBOOLE_0:def 10 :: thesis: D2 c= D1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D1 or x in D2 )
assume x in D1 ; :: thesis: x in D2
then x is Linear_Combination of V by A2;
hence x in D2 by A3; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D2 or x in D1 )
assume x in D2 ; :: thesis: x in D1
then x is Linear_Combination of V by A3;
hence x in D1 by A2; :: thesis: verum