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;>
proof
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;
thus for u being Vector of L holds <;v,u;> = <;w,u;> :: thesis: verum
proof
let u be Vector of L; :: thesis: <;v,u;> = <;w,u;>
thus <;v,u;> = <;u,v;> by ZMODLAT1:def 3
.= <;u,w;> by P1, ZL2LmSc1
.= <;w,u;> by ZMODLAT1:def 3 ; :: thesis: verum
end;