let V be Z_Module; 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; 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; verum