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