theorem Th13: :: ZFREFLE1:13

for W being Universe
for D being non empty set
for Phi being Function of D,(Funcs ((On W),(On W))) st card D in card W holds
ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & phi . (0-element_of W) = 0-element_of W & ( for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) ) & ( for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
phi . a = sup (phi | a) ) )