let V be RealLinearSpace; :: thesis: for v being VECTOR of V
for a being Real
for W being Subspace of V st v in W holds
(a * v) + W = the carrier of W
let v be VECTOR of V; :: thesis: for a being Real
for W being Subspace of V st v in W holds
(a * v) + W = the carrier of W
let a be Real; :: thesis: for W being Subspace of V st v in W holds
(a * v) + W = the carrier of W
let W be Subspace of V; :: thesis: ( v in W implies (a * v) + W = the carrier of W )
assume A1: v in W ; :: thesis: (a * v) + W = the carrier of W
thus (a * v) + W c= the carrier of W :: according to XBOOLE_0:def 10 :: thesis: the carrier of W c= (a * v) + W

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (a * v) + W or x in the carrier of W )
assume x in (a * v) + W ; :: thesis: x in the carrier of W
then consider u being VECTOR of V such that
A2: x = (a * v) + u and
A3: u in W ;
a * v in W by A1, Th29;
then (a * v) + u in W by A3, Th28;
hence x in the carrier of W by A2, STRUCT_0:def 5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of W or x in (a * v) + W )
assume A4: x in the carrier of W ; :: thesis: x in (a * v) + W
( the carrier of W c= the carrier of V & v in V ) by Def2, RLVECT_1:3;
then reconsider y = x as Element of V by A4;
( a * v in W & x in W ) by A1, A4, Th29, STRUCT_0:def 5;
then A5: y - (a * v) in W by Th31;
(a * v) + (y - (a * v)) = (y + (a * v)) - (a * v) by RLVECT_1:def 6
.= y + ((a * v) - (a * v)) by RLVECT_1:def 6
.= y + (0. V) by RLVECT_1:28
.= x by RLVECT_1:10 ;
hence x in (a * v) + W by A5; :: thesis: verum