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

A1: now

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

end;

now

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

end;

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