theorem Th23: :: LOPBAN15:21

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