theorem Th24: :: LOPBAN15:22

for X, Y being RealLinearSpace ex f being LinearOperator of Y,[:((0). X),Y:] st
( f is bijective & ( for y being Element of Y holds f . y = [(0. X),y] ) )