theorem ThSPrEM1: :: ZMODLAT2:9

for L being Z_Lattice
for r being Element of F_Rat
for v, u being Vector of (EMbedding (r,L)) holds ((ScProductDM L) || the carrier of (EMbedding (r,L))) . (v,u) = (ScProductDM L) . (v,u)