theorem Th32: :: VECTSP_9:32

for GF being Field
for V being finite-dimensional VectSp of GF
for W1, W2 being Subspace of V holds (dim (W1 + W2)) + (dim (W1 /\ W2)) = (dim W1) + (dim W2)