let L be positive-definite Z_Lattice; for b being OrdBasis of L
for v, w being Vector of L 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 L; for v, w being Vector of L 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 L; ( ( 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;>
; v = w
reconsider I = rng b as Basis of L by ZMATRLIN:def 5;
for u being Vector of L st u in I holds
<;u,v;> = <;u,w;>
then
<;(v - w),v;> = <;(v - w),w;>
by ZL2LmSc1;
then
<;(v - w),v;> - <;(v - w),w;> = 0. INT.Ring
;
then
||.(v - w).|| = 0. INT.Ring
by ZMODLAT1:11;
then
v - w = 0. L
by ZMODLAT1:16;
hence
v = w
by RLVECT_1:21; verum