theorem ThNonTrivialLat1: :: ZMODLAT1:6

for V being non trivial torsion-free Z_Module
for Z being Submodule of V
for v being non zero Vector of V
for f being Function of [: the carrier of Z, the carrier of Z:], the carrier of F_Real st Z = Lin {v} & ( for v1, v2 being Vector of Z
for a, b being Element of INT.Ring st v1 = a * v & v2 = b * v holds
f . (v1,v2) = a * b ) holds
GenLat (Z,f) is Z_Lattice-like