let K be Field; :: thesis: for V, W being finite-dimensional VectSp of K holds
( dim V = dim W iff ex T being linear-transformation of V,W st T is bijective )
let V, W be finite-dimensional VectSp of K; :: thesis: ( dim V = dim W iff ex T being linear-transformation of V,W st T is bijective )

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

assume A1: dim V = dim W ; :: thesis: ex T being linear-transformation of V,W st T is bijective
consider T1 being linear-transformation of V,((dim V) -VectSp_over K) such that
A2: T1 is bijective by Th64;
consider T2 being linear-transformation of W,((dim V) -VectSp_over K) such that
A3: T2 is bijective by A1, Th64;
consider S being linear-transformation of ((dim V) -VectSp_over K),W such that
A4: ( S = T2 " & S is bijective ) by A3, ZMODUL06:42;
set T = S * T1;
reconsider T = S * T1 as linear-transformation of V,W ;
T is bijective by A2, A4, FINSEQ_4:85;
hence ex T being linear-transformation of V,W st T is bijective ; :: thesis: verum

end;

assume ex T being linear-transformation of V,W st T is bijective ; :: thesis: dim V = dim W
hence dim V = dim W by VECTSP12:4; :: thesis: verum