theorem Th20: :: LOPBAN15:18

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