let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for M being non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF
for W, W', W1 being Subspace of M st the carrier of W = the carrier of W' holds
( W1 /\ W = W1 /\ W' & W /\ W1 = W' /\ W1 )
let M be non empty right_complementable VectSp-like Abelian add-associative right_zeroed VectSpStr of GF; :: thesis: for W, W', W1 being Subspace of M st the carrier of W = the carrier of W' holds
( W1 /\ W = W1 /\ W' & W /\ W1 = W' /\ W1 )
let W, W', W1 be Subspace of M; :: thesis: ( the carrier of W = the carrier of W' implies ( W1 /\ W = W1 /\ W' & W /\ W1 = W' /\ W1 ) )
assume A1: the carrier of W = the carrier of W' ; :: thesis: ( W1 /\ W = W1 /\ W' & W /\ W1 = W' /\ W1 )

A2: now

thus the carrier of (W1 /\ W) = the carrier of W1 /\ the carrier of W' by A1, Def2
.= the carrier of (W1 /\ W') by Def2 ; :: thesis: verum

end;

hence W1 /\ W = W1 /\ W' by VECTSP_4:37; :: thesis: W /\ W1 = W' /\ W1
thus W /\ W1 = W' /\ W1 by A2, VECTSP_4:37; :: thesis: verum