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) . ((b /. n),v) = (ScProductDM L) . ((b /. n),w) ) 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) . ((b /. n),v) = (ScProductDM L) . ((b /. n),w) ) holds
v = w
let v, w be Vector of (DivisibleMod L); :: thesis: ( ( for n being Nat st n in dom b holds
(ScProductDM L) . ((b /. n),v) = (ScProductDM L) . ((b /. n),w) ) implies v = w )
assume A1: for n being Nat st n in dom b holds
(ScProductDM L) . ((b /. n),v) = (ScProductDM L) . ((b /. n),w) ; :: thesis: v = w
consider i being Element of INT.Ring such that
A2: ( i <> 0 & i * v in EMbedding L ) by ZMODUL08:29;
consider j being Element of INT.Ring such that
A3: ( j <> 0 & j * w in EMbedding L ) by ZMODUL08:29;
i * v in rng (MorphsZQ L) by A2, ZMODUL08:def 3;
then reconsider iv = i * v as Vector of (EMLat L) by defEMLat;
j * w in rng (MorphsZQ L) by A3, ZMODUL08:def 3;
then reconsider jw = j * w as Vector of (EMLat L) by defEMLat;
A4: EMLat L is Submodule of DivisibleMod L by ThDivisibleL1;
for n being Nat st n in dom b holds
<;(b /. n),(j * iv);> = <;(b /. n),(i * jw);>

proof

let n be Nat; :: thesis: ( n in dom b implies <;(b /. n),(j * iv);> = <;(b /. n),(i * jw);> )
assume B1: n in dom b ; :: thesis: <;(b /. n),(j * iv);> = <;(b /. n),(i * jw);>
b /. n in EMLat L ;
then b /. n in DivisibleMod L by A4, ZMODUL01:24;
then reconsider bn = b /. n as Vector of (DivisibleMod L) ;
b /. n in EMLat L ;
then b /. n in rng (MorphsZQ L) by defEMLat;
then B2: b /. n in EMbedding L by ZMODUL08:def 3;
B3: (i * j) * ((ScProductDM L) . ((b /. n),v)) = j * (i * ((ScProductDM L) . (bn,v)))
.= j * (i * ((ScProductDM L) . (v,bn))) by ThSPDM1
.= j * ((ScProductDM L) . ((i * v),bn)) by ThSPDM1
.= j * ((ScProductEM L) . (iv,(b /. n))) by A2, B2, ThSPEM3
.= j * <;iv,(b /. n);> by defEMLat
.= <;(j * iv),(b /. n);> by ZMODLAT1:def 3
.= <;(b /. n),(j * iv);> by ZMODLAT1:def 3 ;
(i * j) * ((ScProductDM L) . ((b /. n),w)) = i * (j * ((ScProductDM L) . (bn,w)))
.= i * (j * ((ScProductDM L) . (w,bn))) by ThSPDM1
.= i * ((ScProductDM L) . ((j * w),bn)) by ThSPDM1
.= i * ((ScProductEM L) . (jw,(b /. n))) by A3, B2, ThSPEM3
.= i * <;jw,(b /. n);> by defEMLat
.= <;(i * jw),(b /. n);> by ZMODLAT1:def 3
.= <;(b /. n),(i * jw);> by ZMODLAT1:def 3 ;
hence <;(b /. n),(j * iv);> = <;(b /. n),(i * jw);> by A1, B1, B3; :: thesis: verum

end;

then j * iv = i * jw by ZL2ThSc1
.= i * (j * w) by A4, ZMODUL01:29 ;
then j * (i * v) = i * (j * w) by A4, ZMODUL01:29
.= (i * j) * w by VECTSP_1:def 16 ;
then (i * j) * v = (i * j) * w by VECTSP_1:def 16;
hence v = w by A2, A3, ZMODUL01:10; :: thesis: verum