A1: the scalar of (EMLat (r,L)) =
(ScProductDM L) || (r * (rng (MorphsZQ L)))
by ZMODLAT2:def 5

.= (ScProductDM L) || the carrier of (EMLat (r,L)) by ZMODLAT2:def 5 ;

EMLat (r,L) is Submodule of DivisibleMod L by ZMODLAT2:21;

hence EMLat (r,L) is RATional by A1, ThSLGM1; :: thesis: verum

.= (ScProductDM L) || the carrier of (EMLat (r,L)) by ZMODLAT2:def 5 ;

EMLat (r,L) is Submodule of DivisibleMod L by ZMODLAT2:21;

hence EMLat (r,L) is RATional by A1, ThSLGM1; :: thesis: verum