let L be Z_Lattice; 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); 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); ( v1 = u1 & v2 = u2 implies (ScProductEM L) . (u1,u2) = (ScProductDM L) . (v1,v2) )
assume A1:
( v1 = u1 & v2 = u2 )
; (ScProductEM L) . (u1,u2) = (ScProductDM L) . (v1,v2)
A2:
( u1 = (1. INT.Ring) * v1 & u2 = (1. INT.Ring) * v2 )
by A1, VECTSP_1:def 17;
thus (ScProductDM L) . (v1,v2) =
(((1. F_Real) ") * ((1. F_Real) ")) * ((ScProductEM L) . (u1,u2))
by A2, defScProductDM
.=
(ScProductEM L) . (u1,u2)
; verum