let L be Z_Lattice; 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); (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
; verum