let X, Y be free Z_Module; for T being linear-transformation of X,Y
for A being Subset of X st T is bijective & A is Basis of X holds
T .: A is Basis of Y
let T be linear-transformation of X,Y; for A being Subset of X st T is bijective & A is Basis of X holds
T .: A is Basis of Y
let A be Subset of X; ( T is bijective & A is Basis of X implies T .: A is Basis of Y )
assume AS1:
T is bijective
; ( not A is Basis of X or T .: A is Basis of Y )
assume
A is Basis of X
; T .: A is Basis of Y
then P1:
( A is linearly-independent & Lin A = ModuleStr(# the carrier of X, the addF of X, the ZeroF of X, the lmult of X #) )
by VECTSP_7:def 3;
D1:
dom T = the carrier of X
by FUNCT_2:def 1;
R1:
rng T = the carrier of Y
by FUNCT_2:def 3, AS1;
P2:
T .: A is linearly-independent
by HM6, AS1, P1;
P6:
Lin (T .: A) is strict Subspace of (Omega). Y
by HM8;
the carrier of (Lin (T .: A)) =
T .: the carrier of ModuleStr(# the carrier of X, the addF of X, the ZeroF of X, the lmult of X #)
by P1, AS1, HM7
.=
the carrier of ((Omega). Y)
by D1, R1, RELAT_1:113
;
hence
T .: A is Basis of Y
by P2, VECTSP_7:def 3, P6, ZMODUL01:47; verum