let L be positive-definite Z_Lattice; :: thesis: for b being OrdBasis of EMLat L
for v, w being Vector of (DivisibleMod L) st ( for n being Nat st n in dom b holds
(ScProductDM L) . (v,(b /. n)) = (ScProductDM L) . (w,(b /. n)) ) holds
v = w
let b be OrdBasis of EMLat L; :: thesis: for v, w being Vector of (DivisibleMod L) st ( for n being Nat st n in dom b holds
(ScProductDM L) . (v,(b /. n)) = (ScProductDM L) . (w,(b /. n)) ) holds
v = w
let v, w be Vector of (DivisibleMod L); :: thesis: ( ( for n being Nat st n in dom b holds
(ScProductDM L) . (v,(b /. n)) = (ScProductDM L) . (w,(b /. n)) ) implies v = w )
assume A1: for n being Nat st n in dom b holds
(ScProductDM L) . (v,(b /. n)) = (ScProductDM L) . (w,(b /. n)) ; :: thesis: v = w
for n being Nat st n in dom b holds
(ScProductDM L) . ((b /. n),v) = (ScProductDM L) . ((b /. n),w)

proof

let n be Nat; :: thesis: ( n in dom b implies (ScProductDM L) . ((b /. n),v) = (ScProductDM L) . ((b /. n),w) )
assume B1: n in dom b ; :: thesis: (ScProductDM L) . ((b /. n),v) = (ScProductDM L) . ((b /. n),w)
B2: EMLat L is Submodule of DivisibleMod L by ThDivisibleL1;
b /. n in EMLat L ;
then b /. n in DivisibleMod L by B2, ZMODUL01:24;
then reconsider bn = b /. n as Vector of (DivisibleMod L) ;
thus (ScProductDM L) . ((b /. n),v) = (ScProductDM L) . (v,bn) by ThSPDM1
.= (ScProductDM L) . (w,(b /. n)) by A1, B1
.= (ScProductDM L) . (bn,w) by ThSPDM1
.= (ScProductDM L) . ((b /. n),w) ; :: thesis: verum

end;

hence v = w by ZL2ThSc1D; :: thesis: verum