let L be positive-definite Z_Lattice; :: thesis: for b being OrdBasis of L
for v, w being Vector of L 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 L; :: thesis: for v, w being Vector of L 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 L; :: 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 A2: n in dom b ; :: thesis: <;(b /. n),v;> = <;(b /. n),w;>
thus <;(b /. n),v;> = <;v,(b /. n);> by ZMODLAT1:def 3
.= <;w,(b /. n);> by A1, A2
.= <;(b /. n),w;> by ZMODLAT1:def 3 ; :: thesis: verum

end;

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