theorem Th22: :: LOPBAN15:20

for X, Y being RealLinearSpace
for X1, Y1 being Subspace of [:X,Y:] st X1 = [:X,((0). Y):] & Y1 = [:((0). X),Y:] holds
( X1 + Y1 = [:X,Y:] & X1 /\ Y1 = (0). [:X,Y:] )