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

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