let L be Z_Lattice; :: thesis: for v, u being Vector of L holds
( <;v,(- u);> = - <;v,u;> & <;(- v),u;> = - <;v,u;> )
let v, u be Vector of L; :: thesis: ( <;v,(- u);> = - <;v,u;> & <;(- v),u;> = - <;v,u;> )
thus <;v,(- u);> = <;v,((- (1. INT.Ring)) * u);> by ZMODUL01:2
.= <;((- (1. INT.Ring)) * u),v;> by defZLattice
.= (- 1) * <;u,v;> by defZLattice
.= - <;u,v;>
.= - <;v,u;> by defZLattice ; :: thesis: <;(- v),u;> = - <;v,u;>
thus <;(- v),u;> = <;((- (1. INT.Ring)) * v),u;> by ZMODUL01:2
.= (- (1. INT.Ring)) * <;v,u;> by defZLattice
.= - <;v,u;> ; :: thesis: verum