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