let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for v being VECTOR of V holds {v} is Affine
let v be VECTOR of V; :: thesis: {v} is Affine
for x, y being VECTOR of V
for a being Real st x in {v} & y in {v} holds
((1 - a) * x) + (a * y) in {v}
proof
let x, y be VECTOR of V; :: thesis: for a being Real st x in {v} & y in {v} holds
((1 - a) * x) + (a * y) in {v}
let a be Real; :: thesis: ( x in {v} & y in {v} implies ((1 - a) * x) + (a * y) in {v} )
assume ( x in {v} & y in {v} ) ; :: thesis: ((1 - a) * x) + (a * y) in {v}
then ( x = v & y = v ) by TARSKI:def 1;
then ((1 - a) * x) + (a * y) = ((1 - a) + a) * v by RLVECT_1:def 6
.= v by RLVECT_1:def 8 ;
hence ((1 - a) * x) + (a * y) in {v} by TARSKI:def 1; :: thesis: verum
end;
hence {v} is Affine ; :: thesis: verum