for L being Lattice
for f being Function of the carrier of L, the carrier of L
for x being Element of L holds (f,0) -. x = x