let L be Z_Lattice; :: thesis: for I being Subset of L holds

( I is Basis of L iff (MorphsZQ L) .: I is Basis of (EMbedding L) )

let I be Subset of L; :: thesis: ( I is Basis of L iff (MorphsZQ L) .: I is Basis of (EMbedding L) )

consider T being linear-transformation of L,(EMbedding L) such that

A1: T is bijective and

A2: T = MorphsZQ L and

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

thus ( I is Basis of L iff (MorphsZQ L) .: I is Basis of (EMbedding L) ) by A1, A2, ZMODUL06:49; :: thesis: verum

( I is Basis of L iff (MorphsZQ L) .: I is Basis of (EMbedding L) )

let I be Subset of L; :: thesis: ( I is Basis of L iff (MorphsZQ L) .: I is Basis of (EMbedding L) )

consider T being linear-transformation of L,(EMbedding L) such that

A1: T is bijective and

A2: T = MorphsZQ L and

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

thus ( I is Basis of L iff (MorphsZQ L) .: I is Basis of (EMbedding L) ) by A1, A2, ZMODUL06:49; :: thesis: verum