theorem Th17: :: KNASTER:17

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
for T being Sequence st O <> 0 & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds
T . A = (f,A) +. x ) holds
(f,O) +. x = "\/" ((rng T),L)