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