theorem ThSc6: :: ZMODLAT1:12

for L being Z_Lattice
for v being Vector of L holds
( <;v,(0. L);> = 0 & <;(0. L),v;> = 0 )