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