set Y = { (v + u) where u is Vector of V : u in W } ; defpred S1[ object ] means ex u being Vector of V st ( $1 = v + u & u in W ); consider X being set such that A1:
for x being object holds ( x in X iff ( x in the carrier of V & S1[x] ) )
fromXBOOLE_0:sch 1();
X c= the carrier of V
byA1; then reconsider X = X as Subset of V ; A2:
{ (v + u) where u is Vector of V : u in W } c= X