let D1, D2 be Subset of V; :: thesis: ( ( for x being set holds

( x in D1 iff ex a1, a2 being Vector of V st

( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) ) & ( for x being set holds

( x in D2 iff ex a1, a2 being Vector of V st

( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) ) implies D1 = D2 )

assume that

A2: for x being set holds

( x in D1 iff ex a1, a2 being Vector of V st

( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) and

A3: for x being set holds

( x in D2 iff ex a1, a2 being Vector of V st

( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) ; :: thesis: D1 = D2

( x in D1 iff ex a1, a2 being Vector of V st

( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) ) & ( for x being set holds

( x in D2 iff ex a1, a2 being Vector of V st

( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) ) implies D1 = D2 )

assume that

A2: for x being set holds

( x in D1 iff ex a1, a2 being Vector of V st

( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) and

A3: for x being set holds

( x in D2 iff ex a1, a2 being Vector of V st

( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) ; :: thesis: D1 = D2

now :: thesis: for x being object holds

( x in D1 iff x in D2 )

hence
D1 = D2
by TARSKI:2; :: thesis: verum( x in D1 iff x in D2 )

let x be object ; :: thesis: ( x in D1 iff x in D2 )

( x in D1 iff ex a1, a2 being Vector of V st

( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) by A2;

hence ( x in D1 iff x in D2 ) by A3; :: thesis: verum

end;( x in D1 iff ex a1, a2 being Vector of V st

( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) by A2;

hence ( x in D1 iff x in D2 ) by A3; :: thesis: verum