let V, W be finite-dimensional RealLinearSpace; ( 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
; ( dim V = dim W iff ex T being LinearOperator of V,W st T is bijective )
hereby ( ex T being LinearOperator of V,W st T is bijective implies dim V = dim W )
assume A2:
dim V = dim W
;
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
;
verum
end;
assume
ex T being LinearOperator of V,W st T is bijective
; dim V = dim W
hence
dim V = dim W
by Th88; verum