set S = { (a1 + a2) where a1, a2 is Vector of V : ( a1 in A1 & a2 in A2 ) } ;
A1:
now 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 ;
( 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 ) }
;
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 )
;
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
; 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; verum