let D1, D2 be Subset of V; ( ( 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 ) )
; D1 = D2
now for x being object holds
( x in D1 iff x in D2 )let x be
object ;
( 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;
verum end;
hence
D1 = D2
by TARSKI:2; verum