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

proof

let x be Vector of (DivisibleMod L); :: thesis: ( x in EMbedding L implies (ScProductDM L) . ((v + u),x) in INT.Ring )
assume B1: x in EMbedding L ; :: thesis: (ScProductDM L) . ((v + u),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) . (u,x) in INT.Ring by B1, defDualElement;
then reconsider iu = (ScProductDM L) . (u,x) as Element of INT.Ring ;
set iiv = iv;
set iiu = iu;
(ScProductDM L) . ((v + u),x) = ((ScProductDM L) . (v,x)) + ((ScProductDM L) . (u,x)) by ZMODLAT2:6
.= iv + iu ;
hence (ScProductDM L) . ((v + u),x) in INT.Ring ; :: thesis: verum

end;

hence v + u is Dual of L by defDualElement; :: thesis: verum