set S = { (a1 + a2) where a1, a2 is Vector of V : ( a1 in A1 & a2 in A2 ) } ;

A1: now :: thesis: for x being set st x in { (a1 + a2) where a1, a2 is Vector of V : ( a1 in A1 & a2 in A2 ) } holds
ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 )

let x be set ; :: thesis: ( x in { (a1 + a2) where a1, a2 is Vector of V : ( a1 in A1 & a2 in A2 ) } implies ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 ) )
assume x in { (a1 + a2) where a1, a2 is Vector of V : ( a1 in A1 & a2 in A2 ) } ; :: thesis: ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 )
then ex a1, a2 being Vector of V st
( x = a1 + a2 & a1 in A1 & a2 in A2 ) ;
hence ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 ) ; :: thesis: verum

end;

now :: thesis: for x being object st x in { (a1 + a2) where a1, a2 is Vector of V : ( a1 in A1 & a2 in A2 ) } holds
x in the carrier of V

let x be object ; :: thesis: ( x in { (a1 + a2) where a1, a2 is Vector of V : ( a1 in A1 & a2 in A2 ) } implies x in the carrier of V )
assume x in { (a1 + a2) where a1, a2 is Vector of V : ( a1 in A1 & a2 in A2 ) } ; :: thesis: x in the carrier of V
then ex a1, a2 being Vector of V st
( x = a1 + a2 & a1 in A1 & a2 in A2 ) ;
hence x in the carrier of V ; :: thesis: verum

end;

then reconsider S9 = { (a1 + a2) where a1, a2 is Vector of V : ( a1 in A1 & a2 in A2 ) } as Subset of V by TARSKI:def 3;
take S9 ; :: thesis: for x being set holds
( x in S9 iff ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 ) )
thus for x being set holds
( x in S9 iff ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) by A1; :: thesis: verum