let V be free finite-rank Z_Module; :: thesis: for I being Basis of V ex J being OrdBasis of V st rng J = I
let I be Basis of V; :: thesis: ex J being OrdBasis of V st rng J = I
consider p being FinSequence such that
A2: rng p = I and
A3: p is one-to-one by FINSEQ_4:58;
reconsider p = p as FinSequence of V by A2, FINSEQ_1:def 4;
take f = p; :: thesis: ( f is OrdBasis of V & rng f = I )
thus f is one-to-one by A3; :: according to ZMATRLIN:def 5 :: thesis: ( rng f is Basis of V & rng f = I )
thus ( rng f is Basis of V & rng f = I ) by A2; :: thesis: verum