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

0. V in W by RLSUB_1:17;

hence 0. V in the carrier of W ; :: thesis: verum

( 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

hence
Up W is Affine
; :: thesis: 0. V in the carrier of W
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;((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

0. V in W by RLSUB_1:17;

hence 0. V in the carrier of W ; :: thesis: verum