let R be Ring; :: thesis: for V being LeftMod of R

for W being strict Subspace of V st W <> (0). V holds

ex v being Vector of V st

( v in W & v <> 0. V )

let V be LeftMod of R; :: thesis: for W being strict Subspace of V st W <> (0). V holds

ex v being Vector of V st

( v in W & v <> 0. V )

let W be strict Subspace of V; :: thesis: ( W <> (0). V implies ex v being Vector of V st

( v in W & v <> 0. V ) )

assume A1: W <> (0). V ; :: thesis: ex v being Vector of V st

( v in W & v <> 0. V )

A2: 0. V in W by VECTSP_4:17;

the carrier of W <> {(0. V)} by A1, VECTSP_4:def 3;

then {(0. V)} c< the carrier of W by A2, ZFMISC_1:31;

then consider v being object such that

A3: v in the carrier of W and

A4: not v in {(0. V)} by XBOOLE_0:6;

reconsider v = v as Vector of V by A3, VECTSP_4:10;

take v ; :: thesis: ( v in W & v <> 0. V )

thus ( v in W & v <> 0. V ) by A3, A4, TARSKI:def 1; :: thesis: verum

for W being strict Subspace of V st W <> (0). V holds

ex v being Vector of V st

( v in W & v <> 0. V )

let V be LeftMod of R; :: thesis: for W being strict Subspace of V st W <> (0). V holds

ex v being Vector of V st

( v in W & v <> 0. V )

let W be strict Subspace of V; :: thesis: ( W <> (0). V implies ex v being Vector of V st

( v in W & v <> 0. V ) )

assume A1: W <> (0). V ; :: thesis: ex v being Vector of V st

( v in W & v <> 0. V )

A2: 0. V in W by VECTSP_4:17;

the carrier of W <> {(0. V)} by A1, VECTSP_4:def 3;

then {(0. V)} c< the carrier of W by A2, ZFMISC_1:31;

then consider v being object such that

A3: v in the carrier of W and

A4: not v in {(0. V)} by XBOOLE_0:6;

reconsider v = v as Vector of V by A3, VECTSP_4:10;

take v ; :: thesis: ( v in W & v <> 0. V )

thus ( v in W & v <> 0. V ) by A3, A4, TARSKI:def 1; :: thesis: verum