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

A1: now

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 consider a1, a2 being Vector of V such that
A2: ( x = a1 + a2 & a1 in A1 & a2 in A2 ) ;
thus ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 ) by A2; :: thesis: verum

end;

now

let x be set ; :: 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 consider a1, a2 being Vector of V such that
A3: ( x = a1 + a2 & a1 in A1 & a2 in A2 ) ;
thus x in the carrier of V by A3; :: thesis: verum

end;

then reconsider S' = { (a1 + a2) where a1, a2 is Vector of V : ( a1 in A1 & a2 in A2 ) } as Subset of V by TARSKI:def 3;
take S' ; :: thesis: for x being set holds
( x in S' 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 S' iff ex a1, a2 being Vector of V st
( a1 in A1 & a2 in A2 & x = a1 + a2 ) ) by A1; :: thesis: verum