theorem Th26: :: LOPBAN15:24

for X, Y being finite-dimensional RealLinearSpace holds
( [:X,Y:] is finite-dimensional & dim [:X,Y:] = (dim X) + (dim Y) )