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