let V be non empty Abelian add-associative vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for M, N being Affine Subset of V holds M + N is Affine

let M, N be Affine Subset of V; :: thesis: M + N is Affine

for x, y being VECTOR of V

for a being Real st x in M + N & y in M + N holds

((1 - a) * x) + (a * y) in M + N

let M, N be Affine Subset of V; :: thesis: M + N is Affine

for x, y being VECTOR of V

for a being Real st x in M + N & y in M + N holds

((1 - a) * x) + (a * y) in M + N

proof

hence
M + N is Affine
; :: thesis: verum
let x, y be VECTOR of V; :: thesis: for a being Real st x in M + N & y in M + N holds

((1 - a) * x) + (a * y) in M + N

let a be Real; :: thesis: ( x in M + N & y in M + N implies ((1 - a) * x) + (a * y) in M + N )

assume that

A1: x in M + N and

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

consider u1, v1 being Element of V such that

A3: x = u1 + v1 and

A4: ( u1 in M & v1 in N ) by A1;

consider u2, v2 being Element of V such that

A5: y = u2 + v2 and

A6: ( u2 in M & v2 in N ) by A2;

A7: ((1 - a) * x) + (a * y) = (((1 - a) * u1) + ((1 - a) * v1)) + (a * (u2 + v2)) by A3, A5, RLVECT_1:def 5

.= (((1 - a) * u1) + ((1 - a) * v1)) + ((a * u2) + (a * v2)) by RLVECT_1:def 5

.= ((((1 - a) * u1) + ((1 - a) * v1)) + (a * u2)) + (a * v2) by RLVECT_1:def 3

.= (((1 - a) * v1) + (((1 - a) * u1) + (a * u2))) + (a * v2) by RLVECT_1:def 3

.= (((1 - a) * u1) + (a * u2)) + (((1 - a) * v1) + (a * v2)) by RLVECT_1:def 3 ;

( ((1 - a) * u1) + (a * u2) in M & ((1 - a) * v1) + (a * v2) in N ) by A4, A6, Def4;

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

end;((1 - a) * x) + (a * y) in M + N

let a be Real; :: thesis: ( x in M + N & y in M + N implies ((1 - a) * x) + (a * y) in M + N )

assume that

A1: x in M + N and

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

consider u1, v1 being Element of V such that

A3: x = u1 + v1 and

A4: ( u1 in M & v1 in N ) by A1;

consider u2, v2 being Element of V such that

A5: y = u2 + v2 and

A6: ( u2 in M & v2 in N ) by A2;

A7: ((1 - a) * x) + (a * y) = (((1 - a) * u1) + ((1 - a) * v1)) + (a * (u2 + v2)) by A3, A5, RLVECT_1:def 5

.= (((1 - a) * u1) + ((1 - a) * v1)) + ((a * u2) + (a * v2)) by RLVECT_1:def 5

.= ((((1 - a) * u1) + ((1 - a) * v1)) + (a * u2)) + (a * v2) by RLVECT_1:def 3

.= (((1 - a) * v1) + (((1 - a) * u1) + (a * u2))) + (a * v2) by RLVECT_1:def 3

.= (((1 - a) * u1) + (a * u2)) + (((1 - a) * v1) + (a * v2)) by RLVECT_1:def 3 ;

( ((1 - a) * u1) + (a * u2) in M & ((1 - a) * v1) + (a * v2) in N ) by A4, A6, Def4;

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