let L be Z_Lattice; :: thesis: for v being Vector of L holds
( <;v,(0. L);> = 0 & <;(0. L),v;> = 0 )
let v be Vector of L; :: thesis: ( <;v,(0. L);> = 0 & <;(0. L),v;> = 0 )
thus <;v,(0. L);> = <;v,(v - v);> by RLVECT_1:15
.= <;v,v;> - <;v,v;> by ThSc5
.= 0 ; :: thesis: <;(0. L),v;> = 0
thus <;(0. L),v;> = <;(v - v),v;> by RLVECT_1:15
.= <;v,v;> - <;v,v;> by ThSc5
.= 0 ; :: thesis: verum