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 object ; :: 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, Th21;
then (a * v) + u in W by A3, Th20;
hence x in the carrier of W by A2; :: thesis: verum

end;

let x be object ; :: 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
then A5: x in W ;
the carrier of W c= the carrier of V by Def2;
then reconsider y = x as Element of V by A4;
A6: (a * v) + (y - (a * v)) = (y + (a * v)) - (a * v) by RLVECT_1:def 3
.= y + ((a * v) - (a * v)) by RLVECT_1:def 3
.= y + (0. V) by RLVECT_1:15
.= x ;
a * v in W by A1, Th21;
then y - (a * v) in W by A5, Th23;
hence x in (a * v) + W by A6; :: thesis: verum