take 0. (DivisibleMod L) ; :: thesis: for v being Vector of (DivisibleMod L) st v in EMbedding L holds
(ScProductDM L) . ((0. (DivisibleMod L)),v) in INT.Ring
thus for v being Vector of (DivisibleMod L) st v in EMbedding L holds
(ScProductDM L) . ((0. (DivisibleMod L)),v) in INT.Ring by LmDE00; :: thesis: verum