let V be Z_Module; :: thesis: for sc being Function of [: the carrier of V, the carrier of V:], the carrier of F_Real holds GenLat (V,sc) is Submodule of V
let sc be Function of [: the carrier of V, the carrier of V:], the carrier of F_Real; :: thesis: GenLat (V,sc) is Submodule of V
set L = GenLat (V,sc);
A2: 0. (GenLat (V,sc)) = 0. V ;
A3: the addF of (GenLat (V,sc)) = the addF of V || the carrier of (GenLat (V,sc)) ;
the lmult of (GenLat (V,sc)) = the lmult of V | [: the carrier of INT.Ring, the carrier of (GenLat (V,sc)):] ;
hence GenLat (V,sc) is Submodule of V by A2, A3, VECTSP_4:def 2; :: thesis: verum