theorem ThSPDM1: :: ZMODLAT2:6

for L being Z_Lattice holds
( ( for x being Vector of (DivisibleMod L) st ( for y being Vector of (DivisibleMod L) holds (ScProductDM L) . (x,y) = 0 ) holds
x = 0. (DivisibleMod L) ) & ( for x, y being Vector of (DivisibleMod L) holds (ScProductDM L) . (x,y) = (ScProductDM L) . (y,x) ) & ( for x, y, z being Vector of (DivisibleMod L)
for a being Element of INT.Ring holds
( (ScProductDM L) . ((x + y),z) = ((ScProductDM L) . (x,z)) + ((ScProductDM L) . (y,z)) & (ScProductDM L) . ((a * x),y) = a * ((ScProductDM L) . (x,y)) ) ) )