let K be Field; 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; ( dim V = dim W iff ex T being linear-transformation of V,W st T is bijective )
hereby ( ex T being linear-transformation of V,W st T is bijective implies dim V = dim W )
assume A1:
dim V = dim W
;
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
;
verum
end;
assume
ex T being linear-transformation of V,W st T is bijective
; dim V = dim W
hence
dim V = dim W
by VECTSP12:4; verum