let L be Z_Lattice; :: thesis: for b being FinSequence of L holds

( b is OrdBasis of L iff (MorphsZQ L) * b is OrdBasis of EMbedding L )

let b be FinSequence of L; :: thesis: ( b is OrdBasis of L iff (MorphsZQ L) * b is OrdBasis of EMbedding L )

E1: ex T being linear-transformation of L,(EMbedding L) st

( T is bijective & T = MorphsZQ L & ( for v being Vector of L holds T . v = Class ((EQRZM L),[v,1]) ) ) by ZMODUL08:21;

E4: (MorphsZQ L) * b is FinSequence of (EMbedding L) by E1, FINSEQ_2:32;

P3: rng ((MorphsZQ L) * b) = (MorphsZQ L) .: (rng b) by RELAT_1:127;

then P1: ( (MorphsZQ L) * b is one-to-one & rng ((MorphsZQ L) * b) is Basis of (EMbedding L) ) by ZMATRLIN:def 5;

dom (MorphsZQ L) = the carrier of L by FUNCT_2:def 1;

then rng b c= dom (MorphsZQ L) ;

then P2: b is one-to-one by P1, FUNCT_1:25;

rng b is Basis of L by LmEMDetX6, P1, P3;

hence b is OrdBasis of L by ZMATRLIN:def 5, P2; :: thesis: verum

( b is OrdBasis of L iff (MorphsZQ L) * b is OrdBasis of EMbedding L )

let b be FinSequence of L; :: thesis: ( b is OrdBasis of L iff (MorphsZQ L) * b is OrdBasis of EMbedding L )

E1: ex T being linear-transformation of L,(EMbedding L) st

( T is bijective & T = MorphsZQ L & ( for v being Vector of L holds T . v = Class ((EQRZM L),[v,1]) ) ) by ZMODUL08:21;

E4: (MorphsZQ L) * b is FinSequence of (EMbedding L) by E1, FINSEQ_2:32;

P3: rng ((MorphsZQ L) * b) = (MorphsZQ L) .: (rng b) by RELAT_1:127;

hereby :: thesis: ( (MorphsZQ L) * b is OrdBasis of EMbedding L implies b is OrdBasis of L )

assume
(MorphsZQ L) * b is OrdBasis of EMbedding L
; :: thesis: b is OrdBasis of Lassume
b is OrdBasis of L
; :: thesis: (MorphsZQ L) * b is OrdBasis of EMbedding L

then P1: ( b is one-to-one & rng b is Basis of L ) by ZMATRLIN:def 5;

then (MorphsZQ L) .: (rng b) is Basis of (EMbedding L) by LmEMDetX6;

hence (MorphsZQ L) * b is OrdBasis of EMbedding L by E1, E4, P1, P3, ZMATRLIN:def 5; :: thesis: verum

end;then P1: ( b is one-to-one & rng b is Basis of L ) by ZMATRLIN:def 5;

then (MorphsZQ L) .: (rng b) is Basis of (EMbedding L) by LmEMDetX6;

hence (MorphsZQ L) * b is OrdBasis of EMbedding L by E1, E4, P1, P3, ZMATRLIN:def 5; :: thesis: verum

then P1: ( (MorphsZQ L) * b is one-to-one & rng ((MorphsZQ L) * b) is Basis of (EMbedding L) ) by ZMATRLIN:def 5;

dom (MorphsZQ L) = the carrier of L by FUNCT_2:def 1;

then rng b c= dom (MorphsZQ L) ;

then P2: b is one-to-one by P1, FUNCT_1:25;

rng b is Basis of L by LmEMDetX6, P1, P3;

hence b is OrdBasis of L by ZMATRLIN:def 5, P2; :: thesis: verum