let V be finite-dimensional RealLinearSpace; :: thesis: ( dim V <> 0 implies ex T being LinearOperator of V,(RealVectSpace (Seg (dim V))) st T is bijective )
assume A1: dim V <> 0 ; :: thesis: ex T being LinearOperator of V,(RealVectSpace (Seg (dim V))) st T is bijective
( RLSp2RVSp V is finite-dimensional & dim (RLSp2RVSp V) = dim V ) by Th81;
then consider T being linear-transformation of (RLSp2RVSp V),((dim V) -VectSp_over F_Real) such that
A2: T is bijective by Th64;
(dim V) -VectSp_over F_Real = RLSp2RVSp (RealVectSpace (Seg (dim V))) by Th83, A1;
then reconsider S = T as LinearOperator of V,(RealVectSpace (Seg (dim V))) by Th84;
take S ; :: thesis: S is bijective
the carrier of (RealVectSpace (Seg (dim V))) = the carrier of (RLSp2RVSp (RealVectSpace (Seg (dim V))))
.= the carrier of ((dim V) -VectSp_over F_Real) by Th83, A1 ;
hence S is bijective by A2; :: thesis: verum