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