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)

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

hence
v = w
by ZL2ThSc1D; :: thesis: verum
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;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