theorem Th25: :: LOPBAN15:23

for X, Y being RealLinearSpace
for BX being Basis of X
for BY being Basis of Y holds [:BX,{(0. Y)}:] \/ [:{(0. X)},BY:] is Basis of [:X,Y:]