let V be non empty Abelian add-associative RealLinearSpace-like RLSStruct ; :: thesis: for M being Affine Subset of V
for v being VECTOR of V holds v + M is Affine
let M be Affine Subset of V; :: thesis: for v being VECTOR of V holds v + M is Affine
let v be VECTOR of V; :: thesis: v + M is Affine
for x, y being VECTOR of V
for a being Real st x in v + M & y in v + M holds
((1 - a) * x) + (a * y) in v + M

proof

let x, y be VECTOR of V; :: thesis: for a being Real st x in v + M & y in v + M holds
((1 - a) * x) + (a * y) in v + M
let a be Real; :: thesis: ( x in v + M & y in v + M implies ((1 - a) * x) + (a * y) in v + M )
assume A1: ( x in v + M & y in v + M ) ; :: thesis: ((1 - a) * x) + (a * y) in v + M
then consider x' being Element of V such that
A2: ( x = v + x' & x' in M ) ;
consider y' being Element of V such that
A3: ( y = v + y' & y' in M ) by A1;
A4: ((1 - a) * x') + (a * y') in M by A2, A3, Def5;
((1 - a) * x) + (a * y) = (((1 - a) * v) + ((1 - a) * x')) + (a * (v + y')) by A2, A3, RLVECT_1:def 9
.= (((1 - a) * v) + ((1 - a) * x')) + ((a * v) + (a * y')) by RLVECT_1:def 9
.= ((((1 - a) * v) + ((1 - a) * x')) + (a * v)) + (a * y') by RLVECT_1:def 6
.= (((1 - a) * x') + (((1 - a) * v) + (a * v))) + (a * y') by RLVECT_1:def 6
.= (((1 - a) * x') + (((1 - a) + a) * v)) + (a * y') by RLVECT_1:def 9
.= (((1 - a) * x') + v) + (a * y') by RLVECT_1:def 9
.= v + (((1 - a) * x') + (a * y')) by RLVECT_1:def 6 ;
hence ((1 - a) * x) + (a * y) in v + M by A4; :: thesis: verum

end;

hence v + M is Affine by Def5; :: thesis: verum