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