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