theorem :: LOPBAN15:17

for X being RealLinearSpace
for Y1, Y2 being Subspace of X st Y1 /\ Y2 = (0). X holds
for B1 being linearly-independent Subset of Y1
for B2 being linearly-independent Subset of Y2 holds B1 \/ B2 is linearly-independent Subset of (Y1 + Y2)