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

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