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