for V being 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)