let V be non empty Abelian add-associative RealLinearSpace-like RLSStruct ; :: thesis: for M being Affine Subset of
for v being VECTOR of holds v + M is Affine
let M be Affine Subset of ; :: thesis: for v being VECTOR of holds v + M is Affine
let v be VECTOR of ; :: thesis: v + M is Affine
for x, y being VECTOR of
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 ; :: 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 that
A1: x in v + M and
A2: y in v + M ; :: thesis: ((1 - a) * x) + (a * y) in v + M
consider x' being Element of such that
A3: x = v + x' and
A4: x' in M by A1;
consider y' being Element of such that
A5: y = v + y' and
A6: y' in M by A2;
A7: ((1 - a) * x) + (a * y) = (((1 - a) * v) + ((1 - a) * x')) + (a * (v + y')) by A3, A5, 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 ;
((1 - a) * x') + (a * y') in M by A4, A6, Def5;
hence ((1 - a) * x) + (a * y) in v + M by A7; :: thesis: verum

end;

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