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