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 () 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 () 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 () st v = x & u = y holds
<;v,u;> = <;x,y;>

let x, y be Vector of (); :: 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 () & u in the carrier of () ) by A1;
then A2: ( v in rng () & u in rng () ) by defEMLat;
( v in the carrier of (EMLat (r,L)) & u in the carrier of (EMLat (r,L)) ) ;
then ( v in r * (rng ()) & u in r * (rng ()) ) 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;> = (() || (r * (rng ()))) . (v,u) by defrEMLat
.= (() || the carrier of (EMbedding (r,L))) . (v,u) by ZMODUL08:def 6
.= () . (v,u) by
.= (() || (rng ())) . (v,u) by
.= () . (x,y) by
.= <;x,y;> by defEMLat ; :: thesis: verum