let L be Z_Lattice; :: thesis: rank L = rank (EMLat L)

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

A1: T is bijective and

T = MorphsZQ L and

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

P1: rank L = rank (EMbedding L) by A1, ZMODUL06:51;

ModuleStr(# the carrier of (EMLat L), the addF of (EMLat L), the ZeroF of (EMLat L), the lmult of (EMLat L) #) = EMbedding L by LmEMDetX0;

hence rank L = rank (EMLat L) by P1, LmEMDetX4; :: thesis: verum

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

A1: T is bijective and

T = MorphsZQ L and

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

P1: rank L = rank (EMbedding L) by A1, ZMODUL06:51;

ModuleStr(# the carrier of (EMLat L), the addF of (EMLat L), the ZeroF of (EMLat L), the lmult of (EMLat L) #) = EMbedding L by LmEMDetX0;

hence rank L = rank (EMLat L) by P1, LmEMDetX4; :: thesis: verum