let W be Universe; :: thesis:
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)}:]));
deffunc H₂( set , T-Sequence) -> set = sup $2;
consider L being Ordinal-Sequence such that
A2: ( dom L = On W & ( {} in On W implies L . {} = {} ) ) 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 <> {} & A is limit_ordinal holds
L . A = H₂(A,L | A) from ORDINAL2:sch 11();
defpred S₂[ Ordinal] means L . $1 in On W;
A7: S₂[ 0-element_of W] by A2, ORDINAL1:def 10;
A8: for a being Ordinal of W st S₂[a] holds
S₂[ succ a]

proof

let a be Ordinal of W; :: thesis:
assume L . a in On W ; :: thesis:
then reconsider b = L . a as Ordinal of W by ZF_REFLE:8;
succ a in On W by ZF_REFLE:8;
then A9: L . (succ a) = sup ({b} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) by A3;
card [:D,{(succ a)}:] = card D by CARD_2:13;
then card ((uncurry Phi) .: [:D,{(succ a)}:]) c= card D by CARD_2:2;
then A10: card ((uncurry Phi) .: [:D,{(succ a)}:]) in card W by A1, ORDINAL1:22;
rng Phi c= Funcs (On W),(On W) by RELAT_1:def 19;
then ( rng (uncurry Phi) c= On W & (uncurry Phi) .: [:D,{(succ a)}:] c= rng (uncurry Phi) ) by FUNCT_5:48, RELAT_1:144;
then ( (uncurry Phi) .: [:D,{(succ a)}:] c= On W & On W c= W ) by ORDINAL2:9, XBOOLE_1:1;
then A11: (uncurry Phi) .: [:D,{(succ a)}:] c= W by XBOOLE_1:1;
( {b} in W & (uncurry Phi) .: [:D,{(succ a)}:] in W ) by A10, A11, CLASSES1:2;
then {b} \/ ((uncurry Phi) .: [:D,{(succ a)}:]) in W by CLASSES2:66;
then L . (succ a) in W by A9, ZF_REFLE:28;
hence S₂[ succ a] by ORDINAL1:def 10; :: thesis:

end;

A12: 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]

proof

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

proof

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume e in rng (L | a) ; :: thesis:
then consider u being set such that
A18: ( u in dom (L | a) & e = (L | a) . u ) by FUNCT_1:def 5;
reconsider u = u as Ordinal by A18;
u in On W by A15, A16, A18, ORDINAL1:19;
then reconsider u = u as Ordinal of W by ZF_REFLE:8;
e = L . u by A18, FUNCT_1:70;
then e in On W by A14, A16, A18;
hence e in W by ORDINAL1:def 10; :: thesis:

end;

then L . a in W by A17, Th12, ZF_REFLE:28;
hence S₂[a] by ORDINAL1:def 10; :: thesis:

end;

rng L c= On W

proof

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume e in rng L ; :: thesis:
then consider u being set such that
A19: ( u in dom L & e = L . u ) by FUNCT_1:def 5;
reconsider u = u as Ordinal of W by A2, A19, ZF_REFLE:8;
for a being Ordinal of W holds S₂[a] from ZF_REFLE:sch 4(A7, A8, A12);
then L . u in On W ;
hence e in On W by A19; :: thesis:

end;

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

proof

let A be Ordinal; :: according to ORDINAL2:def 16 :: thesis:
let B be Ordinal; :: thesis:
assume A21: ( A in B & B in dom phi ) ; :: thesis:
then A in dom phi by ORDINAL1:19;
then reconsider a = A, b = B as Ordinal of W by A2, A21, ZF_REFLE:8;
defpred S₃[ Ordinal] means ( a in $1 implies phi . a in phi . $1 );
A22: S₃[ 0-element_of W] ;
A23: for b being Ordinal of W st S₃[b] holds
S₃[ succ b]

proof

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

end;

A26: 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]

proof

let b be Ordinal of W; :: thesis:
assume that
A27: ( 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
A28: a in b ; :: thesis:
( b in On W & a in On W ) by ZF_REFLE:8;
then ( phi . b = sup (phi | b) & phi . a in rng (phi | b) ) by A2, A4, A27, A28, FUNCT_1:73;
hence phi . a in phi . b by ORDINAL2:27; :: thesis:

end;

for b being Ordinal of W holds S₃[b] from ZF_REFLE:sch 4(A22, A23, A26);
then phi . a in phi . b by A21;
hence phi . A in phi . B ; :: thesis:

end;

thus phi is continuous :: thesis:

proof

let A be Ordinal; :: according to ORDINAL2:def 17 :: thesis:
let B be Ordinal; :: thesis:
assume A29: ( A in dom phi & A <> {} & A is limit_ordinal & B = phi . A ) ; :: thesis:
then A c= dom phi by ORDINAL1:def 2;
then ( dom (phi | A) = A & phi | A is increasing & B = sup (phi | A) ) by A2, A4, A20, A29, ORDINAL4:15, RELAT_1:91;
hence B is_limes_of phi | A by A29, ORDINAL4:8; :: thesis:

end;

thus phi . (0-element_of W) = 0-element_of W by A2, ORDINAL1:def 10; :: thesis:
thus for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) :: thesis:

proof

let a be Ordinal of W; :: thesis:
succ a in On W by ZF_REFLE:8;
hence phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) by A3; :: thesis:

end;

let a be Ordinal of W; :: thesis:
a in On W by ZF_REFLE:8;
hence ( a <> 0-element_of W & a is limit_ordinal implies phi . a = sup (phi | a) ) by A4; :: thesis: