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