let L be Z_Lattice; :: thesis: for v, u being Vector of (DivisibleMod L)
for a being Element of INT.Ring holds (ScProductDM L) . (v,(a * u)) = a * ((ScProductDM L) . (v,u))
let v, u be Vector of (DivisibleMod L); :: thesis: for a being Element of INT.Ring holds (ScProductDM L) . (v,(a * u)) = a * ((ScProductDM L) . (v,u))
let a be Element of INT.Ring; :: thesis: (ScProductDM L) . (v,(a * u)) = a * ((ScProductDM L) . (v,u))
thus (ScProductDM L) . (v,(a * u)) = (ScProductDM L) . ((a * u),v) by ThSPDM1
.= a * ((ScProductDM L) . (u,v)) by ThSPDM1
.= a * ((ScProductDM L) . (v,u)) by ThSPDM1 ; :: thesis: verum