theorem ThrEMLat2: :: ZMODLAT2:23
for L being Z_Lattice
for r being Element of F_Rat
for v, u being Vector of (EMLat (r,L))
for x, y being Vector of (EMLat L) st v = x & u = y holds
<;v,u;> = <;x,y;>