theorem ThSc5: :: ZMODLAT1:11

for L being Z_Lattice
for v, u, w being Vector of L holds
( <;(v - u),w;> = <;v,w;> - <;u,w;> & <;v,(u - w);> = <;v,u;> - <;v,w;> )