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