let L be Z_Lattice; :: thesis: for r being Element of F_Rat
for v, u being Vector of (EMLat (r,L))
for x, y being Vector of (EMLat L) st v = x & u = y holds
<;v,u;> = <;x,y;>
let r be Element of F_Rat; :: thesis: for v, u being Vector of (EMLat (r,L))
for x, y being Vector of (EMLat L) st v = x & u = y holds
<;v,u;> = <;x,y;>
let v, u be Vector of (EMLat (r,L)); :: thesis: for x, y being Vector of (EMLat L) st v = x & u = y holds
<;v,u;> = <;x,y;>
let x, y be Vector of (EMLat L); :: thesis: ( v = x & u = y implies <;v,u;> = <;x,y;> )
assume A1: ( v = x & u = y ) ; :: thesis: <;v,u;> = <;x,y;>
( v in the carrier of (EMLat L) & u in the carrier of (EMLat L) ) by A1;
then A2: ( v in rng (MorphsZQ L) & u in rng (MorphsZQ L) ) by defEMLat;
( v in the carrier of (EMLat (r,L)) & u in the carrier of (EMLat (r,L)) ) ;
then ( v in r * (rng (MorphsZQ L)) & u in r * (rng (MorphsZQ L)) ) by defrEMLat;
then A3: ( v is Vector of (EMbedding (r,L)) & u is Vector of (EMbedding (r,L)) ) by ZMODUL08:def 6;
thus <;v,u;> = ((ScProductDM L) || (r * (rng (MorphsZQ L)))) . (v,u) by defrEMLat
.= ((ScProductDM L) || the carrier of (EMbedding (r,L))) . (v,u) by ZMODUL08:def 6
.= (ScProductDM L) . (v,u) by A3, ThSPrEM1
.= ((ScProductDM L) || (rng (MorphsZQ L))) . (v,u) by A2, FUNCT_1:49, ZFMISC_1:87
.= (ScProductEM L) . (x,y) by A1, ThSPEM2
.= <;x,y;> by defEMLat ; :: thesis: verum