let L be Z_Lattice; :: thesis: for L1 being Z_Sublattice of L
for w1, w2 being Vector of L1
for v1, v2 being Vector of L st w1 = v1 & w2 = v2 holds
<;w1,w2;> = <;v1,v2;>
let L1 be Z_Sublattice of L; :: thesis: for w1, w2 being Vector of L1
for v1, v2 being Vector of L st w1 = v1 & w2 = v2 holds
<;w1,w2;> = <;v1,v2;>
let w1, w2 be Vector of L1; :: thesis: for v1, v2 being Vector of L st w1 = v1 & w2 = v2 holds
<;w1,w2;> = <;v1,v2;>
let v1, v2 be Vector of L; :: thesis: ( w1 = v1 & w2 = v2 implies <;w1,w2;> = <;v1,v2;> )
assume B1: ( w1 = v1 & w2 = v2 ) ; :: thesis: <;w1,w2;> = <;v1,v2;>
B2: [w1,w2] in [: the carrier of L1, the carrier of L1:] ;
thus <;w1,w2;> = ( the scalar of L || the carrier of L1) . (w1,w2) by defSublattice
.= <;v1,v2;> by B1, B2, FUNCT_1:49 ; :: thesis: verum