let L be Z_Lattice; :: thesis: for A being non empty set

for ze being Element of A

for ad being BinOp of A

for mu being Function of [: the carrier of INT.Ring,A:],A

for sc being Function of [:A,A:], the carrier of F_Real st A is linearly-closed Subset of (DivisibleMod L) & ze = 0. (DivisibleMod L) & ad = the addF of (DivisibleMod L) || A & mu = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:] holds

LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L

let A be non empty set ; :: thesis: for ze being Element of A

for ad being BinOp of A

for mu being Function of [: the carrier of INT.Ring,A:],A

for sc being Function of [:A,A:], the carrier of F_Real st A is linearly-closed Subset of (DivisibleMod L) & ze = 0. (DivisibleMod L) & ad = the addF of (DivisibleMod L) || A & mu = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:] holds

LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L

let ze be Element of A; :: thesis: for ad being BinOp of A

for mu being Function of [: the carrier of INT.Ring,A:],A

for sc being Function of [:A,A:], the carrier of F_Real st A is linearly-closed Subset of (DivisibleMod L) & ze = 0. (DivisibleMod L) & ad = the addF of (DivisibleMod L) || A & mu = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:] holds

LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L

let ad be BinOp of A; :: thesis: for mu being Function of [: the carrier of INT.Ring,A:],A

for sc being Function of [:A,A:], the carrier of F_Real st A is linearly-closed Subset of (DivisibleMod L) & ze = 0. (DivisibleMod L) & ad = the addF of (DivisibleMod L) || A & mu = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:] holds

LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L

let mu be Function of [: the carrier of INT.Ring,A:],A; :: thesis: for sc being Function of [:A,A:], the carrier of F_Real st A is linearly-closed Subset of (DivisibleMod L) & ze = 0. (DivisibleMod L) & ad = the addF of (DivisibleMod L) || A & mu = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:] holds

LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L

let sc be Function of [:A,A:], the carrier of F_Real; :: thesis: ( A is linearly-closed Subset of (DivisibleMod L) & ze = 0. (DivisibleMod L) & ad = the addF of (DivisibleMod L) || A & mu = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:] implies LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L )

assume A1: ( A is linearly-closed Subset of (DivisibleMod L) & ze = 0. (DivisibleMod L) & ad = the addF of (DivisibleMod L) || A & mu = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:] ) ; :: thesis: LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L

set L1 = LatticeStr(# A,ad,ze,mu,sc #);

set V1 = ModuleStr(# A,ad,ze,mu #);

A2: ModuleStr(# A,ad,ze,mu #) is Submodule of DivisibleMod L by A1, ZMODUL01:40;

reconsider V1 = ModuleStr(# A,ad,ze,mu #) as Z_Module by A1, ZMODUL01:40;

reconsider scc = sc as Function of [: the carrier of V1, the carrier of V1:], the carrier of F_Real ;

LatticeStr(# A,ad,ze,mu,sc #) = GenLat (V1,scc) ;

then LatticeStr(# A,ad,ze,mu,sc #) is Submodule of V1 by ZMODLAT1:2;

hence LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L by A2, ZMODUL01:42; :: thesis: verum

for ze being Element of A

for ad being BinOp of A

for mu being Function of [: the carrier of INT.Ring,A:],A

for sc being Function of [:A,A:], the carrier of F_Real st A is linearly-closed Subset of (DivisibleMod L) & ze = 0. (DivisibleMod L) & ad = the addF of (DivisibleMod L) || A & mu = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:] holds

LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L

let A be non empty set ; :: thesis: for ze being Element of A

for ad being BinOp of A

for mu being Function of [: the carrier of INT.Ring,A:],A

for sc being Function of [:A,A:], the carrier of F_Real st A is linearly-closed Subset of (DivisibleMod L) & ze = 0. (DivisibleMod L) & ad = the addF of (DivisibleMod L) || A & mu = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:] holds

LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L

let ze be Element of A; :: thesis: for ad being BinOp of A

for mu being Function of [: the carrier of INT.Ring,A:],A

for sc being Function of [:A,A:], the carrier of F_Real st A is linearly-closed Subset of (DivisibleMod L) & ze = 0. (DivisibleMod L) & ad = the addF of (DivisibleMod L) || A & mu = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:] holds

LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L

let ad be BinOp of A; :: thesis: for mu being Function of [: the carrier of INT.Ring,A:],A

for sc being Function of [:A,A:], the carrier of F_Real st A is linearly-closed Subset of (DivisibleMod L) & ze = 0. (DivisibleMod L) & ad = the addF of (DivisibleMod L) || A & mu = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:] holds

LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L

let mu be Function of [: the carrier of INT.Ring,A:],A; :: thesis: for sc being Function of [:A,A:], the carrier of F_Real st A is linearly-closed Subset of (DivisibleMod L) & ze = 0. (DivisibleMod L) & ad = the addF of (DivisibleMod L) || A & mu = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:] holds

LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L

let sc be Function of [:A,A:], the carrier of F_Real; :: thesis: ( A is linearly-closed Subset of (DivisibleMod L) & ze = 0. (DivisibleMod L) & ad = the addF of (DivisibleMod L) || A & mu = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:] implies LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L )

assume A1: ( A is linearly-closed Subset of (DivisibleMod L) & ze = 0. (DivisibleMod L) & ad = the addF of (DivisibleMod L) || A & mu = the lmult of (DivisibleMod L) | [: the carrier of INT.Ring,A:] ) ; :: thesis: LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L

set L1 = LatticeStr(# A,ad,ze,mu,sc #);

set V1 = ModuleStr(# A,ad,ze,mu #);

A2: ModuleStr(# A,ad,ze,mu #) is Submodule of DivisibleMod L by A1, ZMODUL01:40;

reconsider V1 = ModuleStr(# A,ad,ze,mu #) as Z_Module by A1, ZMODUL01:40;

reconsider scc = sc as Function of [: the carrier of V1, the carrier of V1:], the carrier of F_Real ;

LatticeStr(# A,ad,ze,mu,sc #) = GenLat (V1,scc) ;

then LatticeStr(# A,ad,ze,mu,sc #) is Submodule of V1 by ZMODLAT1:2;

hence LatticeStr(# A,ad,ze,mu,sc #) is Submodule of DivisibleMod L by A2, ZMODUL01:42; :: thesis: verum