let L be Z_Lattice; :: thesis: for v being Vector of (DivisibleMod L) holds
( (ScProductDM L) . ((0. (DivisibleMod L)),v) = 0 & (ScProductDM L) . (v,(0. (DivisibleMod L))) = 0 )
let v be Vector of (DivisibleMod L); :: thesis: ( (ScProductDM L) . ((0. (DivisibleMod L)),v) = 0 & (ScProductDM L) . (v,(0. (DivisibleMod L))) = 0 )
thus A1: (ScProductDM L) . ((0. (DivisibleMod L)),v) = (ScProductDM L) . ((v - v),v) by RLVECT_1:15
.= ((ScProductDM L) . (v,v)) + ((ScProductDM L) . ((- v),v)) by ThSPDM1
.= ((ScProductDM L) . (v,v)) - ((ScProductDM L) . (v,v)) by ThScDM1
.= 0 ; :: thesis: (ScProductDM L) . (v,(0. (DivisibleMod L))) = 0
thus (ScProductDM L) . (v,(0. (DivisibleMod L))) = 0 by A1, ThSPDM1; :: thesis: verum