let W be Universe; :: thesis: 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 & ( 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) ) )

deffunc H1( set , Sequence) -> set = sup \$2;
let D be non empty set ; :: thesis: 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 & ( 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) ) )

let Phi be Function of D,(Funcs ((On W),(On W))); :: thesis: ( card D in card W implies ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & phi . () = 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) ) ) )

assume A1: card D in card W ; :: thesis: ex phi being Ordinal-Sequence of W st
( phi is increasing & phi is continuous & phi . () = 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) ) )

deffunc H2( 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) = H2(A,L . A) and
A4: for A being Ordinal st A in On W & A <> 0 & A is limit_ordinal holds
L . A = H1(A,L | A) from defpred S2[ Ordinal] means L . \$1 in On W;
A5: for a being Ordinal of W st S2[a] holds
S2[ succ a]
proof
let a be Ordinal of W; :: thesis: ( S2[a] implies S2[ succ a] )
A6: On W c= W by ORDINAL2:7;
assume L . a in On W ; :: thesis: S2[ succ a]
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 ;
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 ;
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 ;
hence S2[ succ a] by ORDINAL1:def 9; :: thesis: verum
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
S2[b] ) holds
S2[a]
proof
let a be Ordinal of W; :: thesis: ( a <> 0-element_of W & a is limit_ordinal & ( for b being Ordinal of W st b in a holds
S2[b] ) implies S2[a] )

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: S2[a]
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
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in rng (L | a) or e in W )
assume e in rng (L | a) ; :: thesis: e in W
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 ;
then reconsider u = u as Ordinal of W by ZF_REFLE:7;
e = L . u by ;
then e in On W by ;
hence e in W by ORDINAL1:def 9; :: thesis: verum
end;
L . a = sup (L | a) by A4, A11, A15;
then L . a in W by ;
hence S2[a] by ORDINAL1:def 9; :: thesis: verum
end;
A19: S2[ 0-element_of W] by ;
rng L c= On W
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in rng L or e in On W )
assume e in rng L ; :: thesis: e in On W
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 ;
for a being Ordinal of W holds S2[a] from then L . u in On W ;
hence e in On W by A21; :: thesis: verum
end;
then reconsider phi = L as Ordinal-Sequence of W by ;
take phi ; :: thesis: ( phi is increasing & phi is continuous & phi . () = 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) ) )

thus A22: phi is increasing :: thesis: ( phi is continuous & phi . () = 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) ) )
proof
let A be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b1 being set holds
( not A in b1 or not b1 in dom phi or phi . A in phi . b1 )

let B be Ordinal; :: thesis: ( not A in B or not B in dom phi or phi . A in phi . B )
assume that
A23: A in B and
A24: B in dom phi ; :: thesis: phi . A in phi . B
A in dom phi by ;
then reconsider a = A, b = B as Ordinal of W by ;
defpred S3[ Ordinal] means ( a in \$1 implies phi . a in phi . \$1 );
A25: for b being Ordinal of W st S3[b] holds
S3[ succ b]
proof
let b be Ordinal of W; :: thesis: ( S3[b] implies S3[ succ b] )
assume A26: ( ( a in b implies phi . a in phi . b ) & a in succ b ) ; :: thesis: phi . a in phi . (succ b)
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 ;
hence phi . a in phi . (succ b) by ; :: thesis: verum
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
S3[c] ) holds
S3[b]
proof
let b be Ordinal of W; :: thesis: ( b <> 0-element_of W & b is limit_ordinal & ( for c being Ordinal of W st c in b holds
S3[c] ) implies S3[b] )

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: phi . a in phi . b
b in On W by ZF_REFLE:7;
then A31: phi . b = sup (phi | b) by ;
a in On W by ZF_REFLE:7;
then phi . a in rng (phi | b) by ;
hence phi . a in phi . b by ; :: thesis: verum
end;
A32: S3[ 0-element_of W] ;
for b being Ordinal of W holds S3[b] from then phi . a in phi . b by A23;
hence phi . A in phi . B ; :: thesis: verum
end;
thus phi is continuous :: thesis: ( phi . () = 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) ) )
proof
let A be Ordinal; :: according to ORDINAL2:def 13 :: thesis: for b1 being set holds
( not A in dom phi or A = 0 or not A is limit_ordinal or not b1 = phi . A or b1 is_limes_of phi | A )

let B be Ordinal; :: thesis: ( not A in dom phi or A = 0 or not A is limit_ordinal or not B = phi . A or B is_limes_of phi | A )
assume that
A33: A in dom phi and
A34: ( A <> 0 & A is limit_ordinal ) and
A35: B = phi . A ; :: thesis: B is_limes_of phi | A
A c= dom phi by ;
then A36: dom (phi | A) = A by RELAT_1:62;
A37: phi | A is increasing by ;
B = sup (phi | A) by A2, A4, A33, A34, A35;
hence B is_limes_of phi | A by ; :: thesis: verum
end;
thus phi . () = 0-element_of W by ; :: thesis: ( ( 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) ) )

thus for a being Ordinal of W holds phi . (succ a) = sup ({(phi . a)} \/ ((uncurry Phi) .: [:D,{(succ a)}:])) by ; :: thesis: for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
phi . a = sup (phi | a)

let a be Ordinal of W; :: thesis: ( a <> 0-element_of W & a is limit_ordinal implies phi . a = sup (phi | a) )
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: verum