let L be Z_Lattice; :: thesis: for v1, v2 being Vector of (DivisibleMod L)
for u1, u2 being Vector of (EMbedding L) st v1 = u1 & v2 = u2 holds
(ScProductEM L) . (u1,u2) = (ScProductDM L) . (v1,v2)
let v1, v2 be Vector of (DivisibleMod L); :: thesis: for u1, u2 being Vector of (EMbedding L) st v1 = u1 & v2 = u2 holds
(ScProductEM L) . (u1,u2) = (ScProductDM L) . (v1,v2)
let u1, u2 be Vector of (EMbedding L); :: thesis: ( v1 = u1 & v2 = u2 implies (ScProductEM L) . (u1,u2) = (ScProductDM L) . (v1,v2) )
assume A1: ( v1 = u1 & v2 = u2 ) ; :: thesis: (ScProductEM L) . (u1,u2) = (ScProductDM L) . (v1,v2)
A2: ( u1 = (1. INT.Ring) * v1 & u2 = (1. INT.Ring) * v2 ) by A1;
thus (ScProductDM L) . (v1,v2) = (((1. F_Real) ") * ((1. F_Real) ")) * ((ScProductEM L) . (u1,u2)) by A2, defScProductDM
.= (ScProductEM L) . (u1,u2) ; :: thesis: verum