let K be Field; :: thesis: for V being finite-dimensional VectSp of K ex T being linear-transformation of V,((dim V) -VectSp_over K) st T is bijective
let V be finite-dimensional VectSp of K; :: thesis: ex T being linear-transformation of V,((dim V) -VectSp_over K) st T is bijective
set b = the OrdBasis of V;
set W = (dim V) -VectSp_over K;
set W0 = (dim V) -Group_over K;
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 |-- the OrdBasis of V ) ) by Th63;
hence ex T being linear-transformation of V,((dim V) -VectSp_over K) st T is bijective ; :: thesis: verum