let L be Z_Lattice; :: thesis: for v being Dual of L
for a being Element of INT.Ring holds a * v is Dual of L
let v be Dual of L; :: thesis: for a being Element of INT.Ring holds a * v is Dual of L
let a be Element of INT.Ring; :: thesis: a * v is Dual of L
for x being Vector of (DivisibleMod L) st x in EMbedding L holds
(ScProductDM L) . ((a * v),x) in INT.Ring

proof

let x be Vector of (DivisibleMod L); :: thesis: ( x in EMbedding L implies (ScProductDM L) . ((a * v),x) in INT.Ring )
assume B1: x in EMbedding L ; :: thesis: (ScProductDM L) . ((a * v),x) in INT.Ring
(ScProductDM L) . (v,x) in INT.Ring by B1, defDualElement;
then reconsider iv = (ScProductDM L) . (v,x) as Element of INT.Ring ;
(ScProductDM L) . ((a * v),x) = a * iv by ZMODLAT2:6;
hence (ScProductDM L) . ((a * v),x) in INT.Ring ; :: thesis: verum

end;

hence a * v is Dual of L by defDualElement; :: thesis: verum