let K be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: for V being VectSp of K

for S, T being Subspace of V

for v being Vector of V st S /\ T = (0). V & v in S & v in T holds

v = 0. V

let V be VectSp of K; :: thesis: for S, T being Subspace of V

for v being Vector of V st S /\ T = (0). V & v in S & v in T holds

v = 0. V

let S, T be Subspace of V; :: thesis: for v being Vector of V st S /\ T = (0). V & v in S & v in T holds

v = 0. V

let v be Vector of V; :: thesis: ( S /\ T = (0). V & v in S & v in T implies v = 0. V )

assume that

A1: S /\ T = (0). V and

A2: ( v in S & v in T ) ; :: thesis: v = 0. V

( v in the carrier of S & v in the carrier of T ) by A2;

then v in the carrier of S /\ the carrier of T by XBOOLE_0:def 4;

then v in the carrier of (S /\ T) by VECTSP_5:def 2;

then v in {(0. V)} by A1, VECTSP_4:def 3;

hence v = 0. V by TARSKI:def 1; :: thesis: verum

for S, T being Subspace of V

for v being Vector of V st S /\ T = (0). V & v in S & v in T holds

v = 0. V

let V be VectSp of K; :: thesis: for S, T being Subspace of V

for v being Vector of V st S /\ T = (0). V & v in S & v in T holds

v = 0. V

let S, T be Subspace of V; :: thesis: for v being Vector of V st S /\ T = (0). V & v in S & v in T holds

v = 0. V

let v be Vector of V; :: thesis: ( S /\ T = (0). V & v in S & v in T implies v = 0. V )

assume that

A1: S /\ T = (0). V and

A2: ( v in S & v in T ) ; :: thesis: v = 0. V

( v in the carrier of S & v in the carrier of T ) by A2;

then v in the carrier of S /\ the carrier of T by XBOOLE_0:def 4;

then v in the carrier of (S /\ T) by VECTSP_5:def 2;

then v in {(0. V)} by A1, VECTSP_4:def 3;

hence v = 0. V by TARSKI:def 1; :: thesis: verum