let V, W be finite-dimensional RealLinearSpace; :: thesis: ( dim V <> 0 implies ( dim V = dim W iff ex T being LinearOperator of V,W st T is bijective ) )
assume A1: dim V <> 0 ; :: thesis: ( dim V = dim W iff ex T being LinearOperator of V,W st T is bijective )

hereby :: thesis: ( ex T being LinearOperator of V,W st T is bijective implies dim V = dim W )

assume A2: dim V = dim W ; :: thesis: ex T being LinearOperator of V,W st T is bijective
consider T1 being LinearOperator of V,(RealVectSpace (Seg (dim V))) such that
A3: T1 is bijective by A1, Th89;
consider T2 being LinearOperator of W,(RealVectSpace (Seg (dim V))) such that
A4: T2 is bijective by A1, A2, Th89;
consider S being LinearOperator of (RealVectSpace (Seg (dim V))),W such that
A5: ( S = T2 " & S is one-to-one & S is onto ) by A4, Th85;
set T = S * T1;
reconsider T = S * T1 as LinearOperator of V,W by Th86;
T is bijective by A3, A5, FINSEQ_4:85;
hence ex T being LinearOperator of V,W st T is bijective ; :: thesis: verum

end;

assume ex T being LinearOperator of V,W st T is bijective ; :: thesis: dim V = dim W
hence dim V = dim W by Th88; :: thesis: verum