theorem Th63: :: REAL_NS2:63

for K being Field
for V being finite-dimensional VectSp of K
for b being OrdBasis of V ex T being linear-transformation of V,((dim V) -VectSp_over K) st
( T is bijective & ( for x being Element of V holds T . x = x |-- b ) )