let L be Z_Lattice; :: thesis: for r being non zero Element of F_Rat
for m, n being Element of INT.Ring
for m1, n1 being Element of INT
for v being Vector of (EMLat (r,L)) st m = m1 & n = n1 & r = m1 / n1 & n1 <> 0 holds
ex x being Vector of () st n * v = m * x

let r be non zero Element of F_Rat; :: thesis: for m, n being Element of INT.Ring
for m1, n1 being Element of INT
for v being Vector of (EMLat (r,L)) st m = m1 & n = n1 & r = m1 / n1 & n1 <> 0 holds
ex x being Vector of () st n * v = m * x

let m, n be Element of INT.Ring; :: thesis: for m1, n1 being Element of INT
for v being Vector of (EMLat (r,L)) st m = m1 & n = n1 & r = m1 / n1 & n1 <> 0 holds
ex x being Vector of () st n * v = m * x

let m1, n1 be Element of INT ; :: thesis: for v being Vector of (EMLat (r,L)) st m = m1 & n = n1 & r = m1 / n1 & n1 <> 0 holds
ex x being Vector of () st n * v = m * x

let v be Vector of (EMLat (r,L)); :: thesis: ( m = m1 & n = n1 & r = m1 / n1 & n1 <> 0 implies ex x being Vector of () st n * v = m * x )
assume A1: ( m = m1 & n = n1 & r = m1 / n1 & n1 <> 0 ) ; :: thesis: ex x being Vector of () st n * v = m * x
consider T being linear-transformation of (),(EMbedding (r,L)) such that
A2: ( ( for u being Element of () st u in EMbedding L holds
T . u = r * u ) & T is bijective ) by ZMODUL08:27;
v in the carrier of (EMLat (r,L)) ;
then v in r * (rng ()) by defrEMLat;
then v in the carrier of (EMbedding (r,L)) by ZMODUL08:def 6;
then v in rng T by ;
then consider ve being object such that
A3: ( ve in the carrier of () & v = T . ve ) by FUNCT_2:11;
reconsider vz = ve as Vector of () by ;
reconsider vd = vz as Vector of () by ZMODUL08:30;
consider zvd being Vector of () such that
A4: ( vd = n * zvd & r * vz = m * zvd ) by ;
A5: vz in EMbedding L by A3;
vz in rng () by ;
then reconsider x = vz as Vector of () by defEMLat;
B1: EMLat L is Submodule of DivisibleMod L by ThDivisibleL1;
B2: EMLat (r,L) is Submodule of DivisibleMod L by ThDivisibleL2;
A7: m * x = m * vd by
.= (m * n) * zvd by
.= n * (m * zvd) by VECTSP_1:def 16
.= n * v by ;
take x ; :: thesis: n * v = m * x
thus n * v = m * x by A7; :: thesis: verum