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