theorem Th15: :: KNASTER:15

for L being Lattice
for f being Function of the carrier of L, the carrier of L
for x being Element of L
for O being Ordinal holds (f,(succ O)) +. x = f . ((f,O) +. x)