let L be Z_Lattice; :: thesis: for v, u, w being Vector of L holds <;v,(u + w);> = <;v,u;> + <;v,w;>
let v, u, w be Vector of L; :: thesis: <;v,(u + w);> = <;v,u;> + <;v,w;>
thus <;v,(u + w);> = <;(u + w),v;> by defZLattice
.= <;u,v;> + <;w,v;> by defZLattice
.= <;v,u;> + <;w,v;> by defZLattice
.= <;v,u;> + <;v,w;> by defZLattice ; :: thesis: verum