theorem FRdsX: :: ZMODUL04:30

for V being Z_Module
for W1, W2 being free Subspace of V st V is_the_direct_sum_of W1,W2 holds
V is free