for x, y being VECTOR of V
for z being Complex st z is Real & x in [#] V & y in [#] V holds
((1r - z) * x) + (z * y) in [#] V ;
hence [#] V is Affine by Def20; :: thesis: verum