let V be RealUnitarySpace; :: thesis: for W being Subspace of V
for v being VECTOR of V
for a being Real st a <> 0 & (a * v) + W = the carrier of W holds
v in W
let W be Subspace of V; :: thesis: for v being VECTOR of V
for a being Real st a <> 0 & (a * v) + W = the carrier of W holds
v in W
let v be VECTOR of V; :: thesis: for a being Real st a <> 0 & (a * v) + W = the carrier of W holds
v in W
let a be Real; :: thesis: ( a <> 0 & (a * v) + W = the carrier of W implies v in W )
assume that
A1: a <> 0 and
A2: (a * v) + W = the carrier of W ; :: thesis: v in W
assume not v in W ; :: thesis: contradiction
then not 1 * v in W by RLVECT_1:def 8;
then not ((a ") * a) * v in W by A1, XCMPLX_0:def 7;
then not (a ") * (a * v) in W by RLVECT_1:def 7;
then A3: not a * v in W by Th15;
( 0. V in W & (a * v) + (0. V) = a * v ) by Th11, RLVECT_1:4;
then a * v in { ((a * v) + u) where u is VECTOR of V : u in W } ;
hence contradiction by A2, A3; :: thesis: verum