let L be Z_Lattice; :: thesis: for r being Element of F_Rat
for v, u being Vector of (EMbedding (r,L)) holds ((ScProductDM L) || the carrier of (EMbedding (r,L))) . (v,u) = (ScProductDM L) . (v,u)
let r be Element of F_Rat; :: thesis: for v, u being Vector of (EMbedding (r,L)) holds ((ScProductDM L) || the carrier of (EMbedding (r,L))) . (v,u) = (ScProductDM L) . (v,u)
let v, u be Vector of (EMbedding (r,L)); :: thesis: ((ScProductDM L) || the carrier of (EMbedding (r,L))) . (v,u) = (ScProductDM L) . (v,u)
set Z = EMbedding (r,L);
EMbedding (r,L) is Submodule of DivisibleMod L by ZMODUL08:32;
then the carrier of (EMbedding (r,L)) c= the carrier of (DivisibleMod L) by VECTSP_4:def 2;
then [: the carrier of (EMbedding (r,L)), the carrier of (EMbedding (r,L)):] c= [: the carrier of (DivisibleMod L), the carrier of (DivisibleMod L):] by ZFMISC_1:96;
then reconsider sc = (ScProductDM L) || the carrier of (EMbedding (r,L)) as Function of [: the carrier of (EMbedding (r,L)), the carrier of (EMbedding (r,L)):], the carrier of F_Real by FUNCT_2:32;
[v,u] in [: the carrier of (EMbedding (r,L)), the carrier of (EMbedding (r,L)):] ;
hence ((ScProductDM L) || the carrier of (EMbedding (r,L))) . (v,u) = (ScProductDM L) . (v,u) by FUNCT_1:49; :: thesis: verum