theorem ThrEMLat1: :: ZMODLAT2:22

for L being Z_Lattice
for r being non zero Element of F_Rat
for m, n being Element of INT.Ring
for m1, n1 being Element of INT
for v being Vector of (EMLat (r,L)) st m = m1 & n = n1 & r = m1 / n1 & n1 <> 0 holds
ex x being Vector of (EMLat L) st n * v = m * x