let F be Field; :: thesis: for U, V being finite-dimensional VectSp of F holds
( U,V are_isomorphic iff dim U = dim V )
let U, V be finite-dimensional VectSp of F; :: thesis: ( U,V are_isomorphic iff dim U = dim V )

now :: thesis: ( dim U = dim V implies U,V are_isomorphic )

assume AS: dim U = dim V ; :: thesis: U,V are_isomorphic

per cases ( dim U = 0 or dim U > 0 ) ;

suppose dim U = 0 ; :: thesis: U,V are_isomorphic

then H0: ( (Omega). U = (0). U & (Omega). V = (0). V ) by AS, VECTSP_9:29;
H1: the carrier of U = {(0. U)} by H0, VECTSP_4:def 3;
H2: the carrier of V = {(0. V)} by H0, VECTSP_4:def 3;
deffunc H₁( object ) -> Element of the carrier of V = 0. V;
H3: for x being object st x in the carrier of U holds
H₁(x) in the carrier of V ;
consider T being Function of the carrier of U, the carrier of V such that
A: for u being object st u in the carrier of U holds
T . u = H₁(u) from FUNCT_2:sch 2(H3);

now :: thesis: for u1, u2 being Element of U holds (T . u1) + (T . u2) = T . (u1 + u2)

let u1, u2 be Element of U; :: thesis: (T . u1) + (T . u2) = T . (u1 + u2)
thus (T . u1) + (T . u2) = (0. V) + (T . u2) by A
.= (0. V) + (0. V) by A
.= T . (u1 + u2) by A ; :: thesis: verum

end;

then B: T is additive by VECTSP_1:def 20;

now :: thesis: for a being Element of F
for u being Element of U holds a * (T . u) = T . (a * u)

let a be Element of F; :: thesis: for u being Element of U holds a * (T . u) = T . (a * u)
let u be Element of U; :: thesis: a * (T . u) = T . (a * u)
thus a * (T . u) = a * (0. V) by A
.= 0. V by VECTSP_1:14
.= T . (a * u) by A ; :: thesis: verum

end;

then C: T is homogeneous by MOD_2:def 2;

now :: thesis: for x1, x2 being object st x1 in the carrier of U & x2 in the carrier of U & T . x1 = T . x2 holds
x1 = x2

let x1, x2 be object ; :: thesis: ( x1 in the carrier of U & x2 in the carrier of U & T . x1 = T . x2 implies x1 = x2 )
assume H4: ( x1 in the carrier of U & x2 in the carrier of U & T . x1 = T . x2 ) ; :: thesis: x1 = x2
hence x1 = 0. U by H1, TARSKI:def 1
.= x2 by H1, H4, TARSKI:def 1 ;
:: thesis: verum

end;

then D: T is one-to-one by FUNCT_2:19;
H5: dom T = the carrier of U by FUNCT_2:def 1;

now :: thesis: for o being object st o in the carrier of V holds
o in rng T

let o be object ; :: thesis: ( o in the carrier of V implies o in rng T )
assume o in the carrier of V ; :: thesis: o in rng T
then o = 0. V by H2, TARSKI:def 1;
then ( T . (0. U) = o & 0. U in dom T ) by H5, A;
hence o in rng T by FUNCT_1:def 3; :: thesis: verum

end;

then ( rng T c= the carrier of V & the carrier of V c= rng T ) ;
then rng T = the carrier of V ;
then T is onto by FUNCT_2:def 3;
hence U,V are_isomorphic by B, C, D; :: thesis: verum

end;

suppose K: dim U > 0 ; :: thesis: U,V are_isomorphic

set Bv = the Basis of V;
card the Basis of V > 0 by AS, K, VECTSP_9:def 1;
then reconsider Bv1 = the Basis of V as non empty Subset of V ;
reconsider U1 = U as non trivial finite-dimensional VectSp of F by K, MATRLIN2:42;
set Bu = the Basis of U1;
card the Basis of U1 = dim V by AS, VECTSP_9:def 1
.= card Bv1 by VECTSP_9:def 1 ;
then consider f1 being Function of the Basis of U1,Bv1 such that
H: f1 is bijective by lemiso;
J: ( dom f1 = the Basis of U1 & rng f1 c= Bv1 & Bv1 c= the carrier of V ) by FUNCT_2:def 1;
then rng f1 c= the carrier of V ;
then reconsider f = f1 as Function of the Basis of U1,V by J, FUNCT_2:2;
set T = canLinTrans f;
rng f is linearly-independent by J, VECTSP_7:1;
then A: canLinTrans f is one-to-one by H, canLininj;

now :: thesis: for o being object st o in the carrier of V holds
o in rng (canLinTrans f)

let o be object ; :: thesis: ( o in the carrier of V implies o in rng (canLinTrans f) )
assume o in the carrier of V ; :: thesis: o in rng (canLinTrans f)
then reconsider v = o as Element of V ;
rng f1 = the Basis of V by H, FUNCT_2:def 3;
then im (canLinTrans f) = Lin Bv1 by canlinsurj;
then ModuleStr(# the carrier of V, the addF of V, the ZeroF of V, the lmult of V #) = im (canLinTrans f) by VECTSP_7:def 3;
then v in im (canLinTrans f) ;
then D: ex x being Element of U st v = (canLinTrans f) . x by RANKNULL:13;
dom (canLinTrans f) = the carrier of U by FUNCT_2:def 1;
hence o in rng (canLinTrans f) by D, FUNCT_1:def 3; :: thesis: verum

end;

then ( rng (canLinTrans f) c= the carrier of V & the carrier of V c= rng (canLinTrans f) ) ;
then canLinTrans f is onto by XBOOLE_0:def 10, FUNCT_2:def 3;
hence U,V are_isomorphic by A; :: thesis: verum

end;

end;

end;

hence ( U,V are_isomorphic iff dim U = dim V ) by VECTSP12:4; :: thesis: verum