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}

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

hence
{v} is Affine
; :: thesis: verum
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;((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