let V be RealLinearSpace; :: thesis: for W being Subspace of V holds
( Up W is Affine & 0. V in the carrier of W )
let W be Subspace of V; :: thesis: ( Up W is Affine & 0. V in the carrier of W )
for x, y being VECTOR of V
for a being Real st x in Up W & y in Up W holds
((1 - a) * x) + (a * y) in Up W

proof

let x, y be VECTOR of V; :: thesis: for a being Real st x in Up W & y in Up W holds
((1 - a) * x) + (a * y) in Up W
let a be Real; :: thesis: ( x in Up W & y in Up W implies ((1 - a) * x) + (a * y) in Up W )
assume that
A1: x in Up W and
A2: y in Up W ; :: thesis: ((1 - a) * x) + (a * y) in Up W
reconsider aa = a as Real ;
y in W by A2;
then A3: aa * y in W by RLSUB_1:21;
x in W by A1;
then (1 - aa) * x in W by RLSUB_1:21;
then ((1 - a) * x) + (a * y) in W by A3, RLSUB_1:20;
hence ((1 - a) * x) + (a * y) in Up W ; :: thesis: verum

end;

hence Up W is Affine ; :: thesis: 0. V in the carrier of W
0. V in W by RLSUB_1:17;
hence 0. V in the carrier of W ; :: thesis: verum