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

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

<;(b /. n),v;> = <;(b /. n),w;> ) holds

v = w

let v, w be Vector of L; :: 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

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;> = 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; :: thesis: verum

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; :: thesis: 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; :: 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

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;>

proof

then
<;(v - w),v;> = <;(v - w),w;>
by ZL2LmSc1;
let u be Vector of L; :: thesis: ( u in I implies <;u,v;> = <;u,w;> )

assume B1: u in I ; :: thesis: <;u,v;> = <;u,w;>

consider i being Nat such that

B2: ( i in dom b & b . i = u ) by B1, FINSEQ_2:10;

b /. i = u by B2, PARTFUN1:def 6;

hence <;u,v;> = <;u,w;> by A1, B2; :: thesis: verum

end;assume B1: u in I ; :: thesis: <;u,v;> = <;u,w;>

consider i being Nat such that

B2: ( i in dom b & b . i = u ) by B1, FINSEQ_2:10;

b /. i = u by B2, PARTFUN1:def 6;

hence <;u,v;> = <;u,w;> by A1, B2; :: thesis: verum

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; :: thesis: verum