let R be Ring; :: thesis: for V being LeftMod of R
for W1, W2 being Subspace of V
for W1s, W2s being strict Subspace of V st W1s = (Omega). W1 & W2s = (Omega). W2 holds
W1s /\ W2s = W1 /\ W2

let V be LeftMod of R; :: thesis: for W1, W2 being Subspace of V
for W1s, W2s being strict Subspace of V st W1s = (Omega). W1 & W2s = (Omega). W2 holds
W1s /\ W2s = W1 /\ W2

let W1, W2 be Subspace of V; :: thesis: for W1s, W2s being strict Subspace of V st W1s = (Omega). W1 & W2s = (Omega). W2 holds
W1s /\ W2s = W1 /\ W2

let W1s, W2s be strict Subspace of V; :: thesis: ( W1s = (Omega). W1 & W2s = (Omega). W2 implies W1s /\ W2s = W1 /\ W2 )
assume A1: ( W1s = (Omega). W1 & W2s = (Omega). W2 ) ; :: thesis: W1s /\ W2s = W1 /\ W2
for x being Vector of V holds
( x in W1 /\ W2 iff x in W1s /\ W2s )
proof
let x be Vector of V; :: thesis: ( x in W1 /\ W2 iff x in W1s /\ W2s )
hereby :: thesis: ( x in W1s /\ W2s implies x in W1 /\ W2 )
assume x in W1 /\ W2 ; :: thesis: x in W1s /\ W2s
then B1: ( x in W1 & x in W2 ) by VECTSP_5:3;
B2: x in W1s by A1, B1;
x in W2s by A1, B1;
hence x in W1s /\ W2s by ; :: thesis: verum
end;
assume B1: x in W1s /\ W2s ; :: thesis: x in W1 /\ W2
x in ModuleStr(# the carrier of W1, the addF of W1, the ZeroF of W1, the lmult of W1 #) by ;
then B2: x in W1 ;
x in ModuleStr(# the carrier of W2, the addF of W2, the ZeroF of W2, the lmult of W2 #) by ;
then x in W2 ;
hence x in W1 /\ W2 by ; :: thesis: verum
end;
hence W1 /\ W2 = W1s /\ W2s by VECTSP_4:30; :: thesis: verum