let L be positive-definite Z_Lattice; :: thesis: for I being Basis of L

for v, w being Vector of L st ( for u being Vector of L st u in I holds

<;v,u;> = <;w,u;> ) holds

for u being Vector of L holds <;v,u;> = <;w,u;>

let I be Basis of L; :: thesis: for v, w being Vector of L st ( for u being Vector of L st u in I holds

<;v,u;> = <;w,u;> ) holds

for u being Vector of L holds <;v,u;> = <;w,u;>

let v, w be Vector of L; :: thesis: ( ( for u being Vector of L st u in I holds

<;v,u;> = <;w,u;> ) implies for u being Vector of L holds <;v,u;> = <;w,u;> )

assume AS: for u being Vector of L st u in I holds

<;v,u;> = <;w,u;> ; :: thesis: for u being Vector of L holds <;v,u;> = <;w,u;>

P1: for u being Vector of L st u in I holds

<;u,v;> = <;u,w;>

for v, w being Vector of L st ( for u being Vector of L st u in I holds

<;v,u;> = <;w,u;> ) holds

for u being Vector of L holds <;v,u;> = <;w,u;>

let I be Basis of L; :: thesis: for v, w being Vector of L st ( for u being Vector of L st u in I holds

<;v,u;> = <;w,u;> ) holds

for u being Vector of L holds <;v,u;> = <;w,u;>

let v, w be Vector of L; :: thesis: ( ( for u being Vector of L st u in I holds

<;v,u;> = <;w,u;> ) implies for u being Vector of L holds <;v,u;> = <;w,u;> )

assume AS: for u being Vector of L st u in I holds

<;v,u;> = <;w,u;> ; :: thesis: for u being Vector of L holds <;v,u;> = <;w,u;>

P1: for u being Vector of L st u in I holds

<;u,v;> = <;u,w;>

proof

thus
for u being Vector of L holds <;v,u;> = <;w,u;>
:: thesis: verum
let u be Vector of L; :: thesis: ( u in I implies <;u,v;> = <;u,w;> )

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

thus <;u,v;> = <;v,u;> by ZMODLAT1:def 3

.= <;w,u;> by AS, P0

.= <;u,w;> by ZMODLAT1:def 3 ; :: thesis: verum

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

thus <;u,v;> = <;v,u;> by ZMODLAT1:def 3

.= <;w,u;> by AS, P0

.= <;u,w;> by ZMODLAT1:def 3 ; :: thesis: verum