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

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

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 )

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;( 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

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

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;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;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

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