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
() . (v,(b /. n)) = () . (w,(b /. n)) ) 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
() . (v,(b /. n)) = () . (w,(b /. n)) ) holds
v = w

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

assume A1: for n being Nat st n in dom b holds
() . (v,(b /. n)) = () . (w,(b /. n)) ; :: thesis: v = w
for n being Nat st n in dom b holds
() . ((b /. n),v) = () . ((b /. n),w)
proof
let n be Nat; :: thesis: ( n in dom b implies () . ((b /. n),v) = () . ((b /. n),w) )
assume B1: n in dom b ; :: thesis: () . ((b /. n),v) = () . ((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 ;
then reconsider bn = b /. n as Vector of () ;
thus () . ((b /. n),v) = () . (v,bn) by ThSPDM1
.= () . (w,(b /. n)) by A1, B1
.= () . (bn,w) by ThSPDM1
.= () . ((b /. n),w) ; :: thesis: verum
end;
hence v = w by ZL2ThSc1D; :: thesis: verum