let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital 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

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

hence
v + M is Affine
; :: thesis: verum
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 that

A1: x in v + M and

A2: y in v + M ; :: thesis: ((1 - a) * x) + (a * y) in v + M

consider x9 being Element of V such that

A3: x = v + x9 and

A4: x9 in M by A1;

consider y9 being Element of V such that

A5: y = v + y9 and

A6: y9 in M by A2;

A7: ((1 - a) * x) + (a * y) = (((1 - a) * v) + ((1 - a) * x9)) + (a * (v + y9)) by A3, A5, RLVECT_1:def 5

.= (((1 - a) * v) + ((1 - a) * x9)) + ((a * v) + (a * y9)) by RLVECT_1:def 5

.= ((((1 - a) * v) + ((1 - a) * x9)) + (a * v)) + (a * y9) by RLVECT_1:def 3

.= (((1 - a) * x9) + (((1 - a) * v) + (a * v))) + (a * y9) by RLVECT_1:def 3

.= (((1 - a) * x9) + (((1 - a) + a) * v)) + (a * y9) by RLVECT_1:def 6

.= (((1 - a) * x9) + v) + (a * y9) by RLVECT_1:def 8

.= v + (((1 - a) * x9) + (a * y9)) by RLVECT_1:def 3 ;

((1 - a) * x9) + (a * y9) in M by A4, A6, Def4;

hence ((1 - a) * x) + (a * y) in v + M by A7; :: thesis: verum

end;((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 x9 being Element of V such that

A3: x = v + x9 and

A4: x9 in M by A1;

consider y9 being Element of V such that

A5: y = v + y9 and

A6: y9 in M by A2;

A7: ((1 - a) * x) + (a * y) = (((1 - a) * v) + ((1 - a) * x9)) + (a * (v + y9)) by A3, A5, RLVECT_1:def 5

.= (((1 - a) * v) + ((1 - a) * x9)) + ((a * v) + (a * y9)) by RLVECT_1:def 5

.= ((((1 - a) * v) + ((1 - a) * x9)) + (a * v)) + (a * y9) by RLVECT_1:def 3

.= (((1 - a) * x9) + (((1 - a) * v) + (a * v))) + (a * y9) by RLVECT_1:def 3

.= (((1 - a) * x9) + (((1 - a) + a) * v)) + (a * y9) by RLVECT_1:def 6

.= (((1 - a) * x9) + v) + (a * y9) by RLVECT_1:def 8

.= v + (((1 - a) * x9) + (a * y9)) by RLVECT_1:def 3 ;

((1 - a) * x9) + (a * y9) in M by A4, A6, Def4;

hence ((1 - a) * x) + (a * y) in v + M by A7; :: thesis: verum