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

let b be OrdBasis of EMLat L; :: thesis: for v, w being Vector of () st ( for n being Nat st n in dom b holds
() . ((b /. n),v) = () . ((b /. n),w) ) holds
v = w

let v, w be Vector of (); :: thesis: ( ( for n being Nat st n in dom b holds
() . ((b /. n),v) = () . ((b /. n),w) ) implies v = w )

assume A1: for n being Nat st n in dom b holds
() . ((b /. n),v) = () . ((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 () by ;
then reconsider iv = i * v as Vector of () by defEMLat;
j * w in rng () by ;
then reconsider jw = j * w as Vector of () 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 ;
then reconsider bn = b /. n as Vector of () ;
b /. n in EMLat L ;
then b /. n in rng () by defEMLat;
then B2: b /. n in EMbedding L by ZMODUL08:def 3;
B3: (i * j) * (() . ((b /. n),v)) = j * (i * (() . (bn,v)))
.= j * (i * (() . (v,bn))) by ThSPDM1
.= j * (() . ((i * v),bn)) by ThSPDM1
.= j * (() . (iv,(b /. n))) by
.= j * <;iv,(b /. n);> by defEMLat
.= <;(j * iv),(b /. n);> by ZMODLAT1:def 3
.= <;(b /. n),(j * iv);> by ZMODLAT1:def 3 ;
(i * j) * (() . ((b /. n),w)) = i * (j * (() . (bn,w)))
.= i * (j * (() . (w,bn))) by ThSPDM1
.= i * (() . ((j * w),bn)) by ThSPDM1
.= i * (() . (jw,(b /. n))) by
.= 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 ;
then j * (i * v) = i * (j * w) by
.= (i * j) * w by VECTSP_1:def 16 ;
then (i * j) * v = (i * j) * w by VECTSP_1:def 16;
hence v = w by ; :: thesis: verum