let W be Universe; :: thesis:
deffunc H₁( set , Sequence) -> set = sup $2;
let D be non empty set ; :: thesis:
let Phi be Function of D,(Funcs ((On W),(On W))); :: thesis:
assume A1: card D in card W ; :: thesis:
deffunc H₂( Ordinal, Ordinal) -> set = sup ({$2} \/ ((uncurry Phi) .: [:D,{(succ $1)}:]));
consider L being Ordinal-Sequence such that
A2: ( dom L = On W & ( 0 in On W implies L . 0 = 0 ) ) and
A3: for A being Ordinal st succ A in On W holds
L . (succ A) = H₂(A,L . A) and
A4: for A being Ordinal st A in On W & A <> 0 & A is limit_ordinal holds
L . A = H₁(A,L | A) from ORDINAL2:sch 11();
defpred S₂[ Ordinal] means L . $1 in On W;
A5: for a being Ordinal of W st S₂[a] holds
S₂[ succ a]

let a be Ordinal of W; :: thesis:
A6: On W c= W by ORDINAL2:7;
assume L . a in On W ; :: thesis:
then reconsider b = L . a as Ordinal of W by ZF_REFLE:7;
card [:D,{(succ a)}:] = card D by CARD_1:69;
then card ((uncurry Phi) .: [:D,{(succ a)}:]) c= card D by CARD_1:66;
then A7: card ((uncurry Phi) .: [:D,{(succ a)}:]) in card W by A1, ORDINAL1:12;
rng Phi c= Funcs ((On W),(On W)) by RELAT_1:def 19;
then A8: rng (uncurry Phi) c= On W by FUNCT_5:41;
(uncurry Phi) .: [:D,{(succ a)}:] c= rng (uncurry Phi) by RELAT_1:111;
then (uncurry Phi) .: [:D,{(succ a)}:] c= On W by A8;
then (uncurry Phi) .: [:D,{(succ a)}:] c= W by A6;
then (uncurry Phi) .: [:D,{(succ a)}:] in W by A7, CLASSES1:1;
then A9: {b} \/ ((uncurry Phi) .: [:D,{(succ a)}:]) in W by CLASSES2:60;
succ a in On W by ZF_REFLE:7;
then L . (succ a) = sup ({b} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) by A3;
then L . (succ a) in W by A9, ZF_REFLE:19;
hence S₂[ succ a] by ORDINAL1:def 9; :: thesis:

end;

A10: for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal & ( for b being Ordinal of W st b in a holds
S₂[b] ) holds
S₂[a]

let a be Ordinal of W; :: thesis:
assume that
A11: ( a <> 0-element_of W & a is limit_ordinal ) and
A12: for b being Ordinal of W st b in a holds
L . b in On W ; :: thesis:
A13: dom (L | a) c= a by RELAT_1:58;
then A14: dom (L | a) in W by CLASSES1:def 1;
A15: a in On W by ZF_REFLE:7;
A16: rng (L | a) c= W

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in rng (L | a) ; :: thesis:
then consider u being object such that
A17: u in dom (L | a) and
A18: e = (L | a) . u by FUNCT_1:def 3;
reconsider u = u as Ordinal by A17;
u in On W by A15, A13, A17, ORDINAL1:10;
then reconsider u = u as Ordinal of W by ZF_REFLE:7;
e = L . u by A17, A18, FUNCT_1:47;
then e in On W by A12, A13, A17;
hence e in W by ORDINAL1:def 9; :: thesis:

end;

L . a = sup (L | a) by A4, A11, A15;
then L . a in W by A14, A16, Th11, ZF_REFLE:19;
hence S₂[a] by ORDINAL1:def 9; :: thesis:

end;

A19: S₂[ 0-element_of W] by A2, ORDINAL1:def 9;
rng L c= On W

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in rng L ; :: thesis:
then consider u being object such that
A20: u in dom L and
A21: e = L . u by FUNCT_1:def 3;
reconsider u = u as Ordinal of W by A2, A20, ZF_REFLE:7;
for a being Ordinal of W holds S₂[a] from ZF_REFLE:sch 4(A19, A5, A10);
then L . u in On W ;
hence e in On W by A21; :: thesis:

end;

then reconsider phi = L as Ordinal-Sequence of W by A2, FUNCT_2:def 1, RELSET_1:4;
take phi ; :: thesis:
thus A22: phi is increasing :: thesis:

let A be Ordinal; :: according to ORDINAL2:def 12 :: thesis:
let B be Ordinal; :: thesis:
assume that
A23: A in B and
A24: B in dom phi ; :: thesis:
A in dom phi by A23, A24, ORDINAL1:10;
then reconsider a = A, b = B as Ordinal of W by A2, A24, ZF_REFLE:7;
defpred S₃[ Ordinal] means ( a in $1 implies phi . a in phi . $1 );
A25: for b being Ordinal of W st S₃[b] holds
S₃[ succ b]

let b be Ordinal of W; :: thesis:
assume A26: ( ( a in b implies phi . a in phi . b ) & a in succ b ) ; :: thesis:
phi . b in {(phi . b)} by TARSKI:def 1;
then A27: phi . b in {(phi . b)} \/ ((uncurry Phi) .: [:D,{(succ b)}:]) by XBOOLE_0:def 3;
succ b in On W by ZF_REFLE:7;
then phi . (succ b) = sup ({(phi . b)} \/ ((uncurry Phi) .: [:D,{(succ b)}:])) by A3;
then phi . b in phi . (succ b) by A27, ORDINAL2:19;
hence phi . a in phi . (succ b) by A26, ORDINAL1:8, ORDINAL1:10; :: thesis:

end;

A28: for b being Ordinal of W st b <> 0-element_of W & b is limit_ordinal & ( for c being Ordinal of W st c in b holds
S₃[c] ) holds
S₃[b]

let b be Ordinal of W; :: thesis:
assume that
A29: ( b <> 0-element_of W & b is limit_ordinal ) and
for c being Ordinal of W st c in b & a in c holds
phi . a in phi . c and
A30: a in b ; :: thesis:
b in On W by ZF_REFLE:7;
then A31: phi . b = sup (phi | b) by A4, A29;
a in On W by ZF_REFLE:7;
then phi . a in rng (phi | b) by A2, A30, FUNCT_1:50;
hence phi . a in phi . b by A31, ORDINAL2:19; :: thesis:

end;

A32: S₃[ 0-element_of W] ;
for b being Ordinal of W holds S₃[b] from ZF_REFLE:sch 4(A32, A25, A28);
then phi . a in phi . b by A23;
hence phi . A in phi . B ; :: thesis:

end;

thus phi is continuous :: thesis:

let A be Ordinal; :: according to ORDINAL2:def 13 :: thesis:
let B be Ordinal; :: thesis:
assume that
A33: A in dom phi and
A34: ( A <> 0 & A is limit_ordinal ) and
A35: B = phi . A ; :: thesis:
A c= dom phi by A33, ORDINAL1:def 2;
then A36: dom (phi | A) = A by RELAT_1:62;
A37: phi | A is increasing by A22, ORDINAL4:15;
B = sup (phi | A) by A2, A4, A33, A34, A35;
hence B is_limes_of phi | A by A34, A36, A37, ORDINAL4:8; :: thesis:

end;

thus phi . (0-element_of W) = 0-element_of W by A2, ORDINAL1:def 9; :: thesis:
thus for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) by A3, ZF_REFLE:7; :: thesis:
let a be Ordinal of W; :: thesis:
a in On W by ZF_REFLE:7;
hence ( a <> 0-element_of W & a is limit_ordinal implies phi . a = sup (phi | a) ) by A4; :: thesis: