theorem ThTrivialLat1: :: ZMODLAT1:5

for V being free finite-rank Z_Module
for f being Function of [: the carrier of ((0). V), the carrier of ((0). V):], the carrier of F_Real st f = [: the carrier of ((0). V), the carrier of ((0). V):] --> (0. F_Real) holds
GenLat (((0). V),f) is Z_Lattice-like