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

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

hence
v = w
by ZL2ThSc1; :: thesis: verum
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;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