let L be positive-definite Z_Lattice; :: thesis: for v being Vector of () holds
( () . (v,v) = 0 iff v = 0. () )

let v be Vector of (); :: thesis: ( () . (v,v) = 0 iff v = 0. () )
consider a being Element of INT.Ring such that
A1: ( a <> 0 & a * v in EMbedding L ) by ZMODUL08:29;
a1: a <> 0. INT.Ring by A1;
reconsider u = a * v as Vector of () by A1;
u in the carrier of () ;
then u in rng () by ZMODUL08:def 3;
then reconsider ul = u as Vector of () by defEMLat;
A2: (a * a) * (() . (v,v)) = a * (a * (() . (v,v)))
.= a * (() . ((a * v),v)) by ThSPDM1
.= a * (() . (v,(a * v))) by ThSPDM1
.= () . ((a * v),(a * v)) by ThSPDM1 ;
ScProductEM L = () || (rng ()) by ThSPEM2
.= () || the carrier of () by ZMODUL08:def 3 ;
then A4: () . ((a * v),(a * v)) = () . (u,u) by
.= ||.ul.|| by defEMLat ;
hereby :: thesis: ( v = 0. () implies () . (v,v) = 0 ) end;
assume v = 0. () ; :: thesis: () . (v,v) = 0
then u = 0. () by ZMODUL01:1
.= zeroCoset L by ZMODUL08:def 4
.= 0. () by defEMLat ;
hence (ScProductDM L) . (v,v) = 0 by ; :: thesis: verum