let L be Z_Lattice; :: thesis: for v being Vector of (DivisibleMod L)

for I being Basis of (EMbedding L) st ( for u being Vector of (DivisibleMod L) st u in I holds

(ScProductDM L) . (v,u) = 0 ) holds

v = 0. (DivisibleMod L)

let v be Vector of (DivisibleMod L); :: thesis: for I being Basis of (EMbedding L) st ( for u being Vector of (DivisibleMod L) st u in I holds

(ScProductDM L) . (v,u) = 0 ) holds

v = 0. (DivisibleMod L)

let I be Basis of (EMbedding L); :: thesis: ( ( for u being Vector of (DivisibleMod L) st u in I holds

(ScProductDM L) . (v,u) = 0 ) implies v = 0. (DivisibleMod L) )

assume A1: for u being Vector of (DivisibleMod L) st u in I holds

(ScProductDM L) . (v,u) = 0 ; :: thesis: v = 0. (DivisibleMod L)

for u being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,u) = 0 by A1, LmDE22;

hence v = 0. (DivisibleMod L) by ThSPDM1; :: thesis: verum

for I being Basis of (EMbedding L) st ( for u being Vector of (DivisibleMod L) st u in I holds

(ScProductDM L) . (v,u) = 0 ) holds

v = 0. (DivisibleMod L)

let v be Vector of (DivisibleMod L); :: thesis: for I being Basis of (EMbedding L) st ( for u being Vector of (DivisibleMod L) st u in I holds

(ScProductDM L) . (v,u) = 0 ) holds

v = 0. (DivisibleMod L)

let I be Basis of (EMbedding L); :: thesis: ( ( for u being Vector of (DivisibleMod L) st u in I holds

(ScProductDM L) . (v,u) = 0 ) implies v = 0. (DivisibleMod L) )

assume A1: for u being Vector of (DivisibleMod L) st u in I holds

(ScProductDM L) . (v,u) = 0 ; :: thesis: v = 0. (DivisibleMod L)

for u being Vector of (DivisibleMod L) holds (ScProductDM L) . (v,u) = 0 by A1, LmDE22;

hence v = 0. (DivisibleMod L) by ThSPDM1; :: thesis: verum