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 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; :: thesis: 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; :: thesis: verum