let GF be Field; :: thesis: for V being VectSp of GF

for a being Element of GF

for v being Element of V

for W being Subspace of V st a <> 0. GF & (a * v) + W = the carrier of W holds

v in W

let V be VectSp of GF; :: thesis: for a being Element of GF

for v being Element of V

for W being Subspace of V st a <> 0. GF & (a * v) + W = the carrier of W holds

v in W

let a be Element of GF; :: thesis: for v being Element of V

for W being Subspace of V st a <> 0. GF & (a * v) + W = the carrier of W holds

v in W

let v be Element of V; :: thesis: for W being Subspace of V st a <> 0. GF & (a * v) + W = the carrier of W holds

v in W

let W be Subspace of V; :: thesis: ( a <> 0. GF & (a * v) + W = the carrier of W implies v in W )

assume that

A1: a <> 0. GF and

A2: (a * v) + W = the carrier of W ; :: thesis: v in W

assume not v in W ; :: thesis: contradiction

then not (1_ GF) * v in W by VECTSP_1:def 17;

then not ((a ") * a) * v in W by A1, VECTSP_1:def 10;

then not (a ") * (a * v) in W by VECTSP_1:def 16;

then A3: not a * v in W by Th21;

( 0. V in W & (a * v) + (0. V) = a * v ) by Th17, 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

for a being Element of GF

for v being Element of V

for W being Subspace of V st a <> 0. GF & (a * v) + W = the carrier of W holds

v in W

let V be VectSp of GF; :: thesis: for a being Element of GF

for v being Element of V

for W being Subspace of V st a <> 0. GF & (a * v) + W = the carrier of W holds

v in W

let a be Element of GF; :: thesis: for v being Element of V

for W being Subspace of V st a <> 0. GF & (a * v) + W = the carrier of W holds

v in W

let v be Element of V; :: thesis: for W being Subspace of V st a <> 0. GF & (a * v) + W = the carrier of W holds

v in W

let W be Subspace of V; :: thesis: ( a <> 0. GF & (a * v) + W = the carrier of W implies v in W )

assume that

A1: a <> 0. GF and

A2: (a * v) + W = the carrier of W ; :: thesis: v in W

assume not v in W ; :: thesis: contradiction

then not (1_ GF) * v in W by VECTSP_1:def 17;

then not ((a ") * a) * v in W by A1, VECTSP_1:def 10;

then not (a ") * (a * v) in W by VECTSP_1:def 16;

then A3: not a * v in W by Th21;

( 0. V in W & (a * v) + (0. V) = a * v ) by Th17, 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