let W be Universe; :: thesis:
deffunc H₁( Ordinal, set ) -> set = Rank $1;
deffunc H₂( Ordinal, set ) -> set = Rank (succ $1);
consider L being Sequence such that
A1: ( dom L = On W & ( 0 in On W implies L . 0 = Rank (1-element_of W) ) ) and
A2: for A being Ordinal st succ A in On W holds
L . (succ A) = H₂(A,L . A) and
A3: 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 5();
A4: for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Rank a by A3, ZF_REFLE:7;
A5: for a being Ordinal of W holds L . (succ a) = Rank (succ a) by A2, ZF_REFLE:7;
A6: for a being Ordinal of W st a <> {} holds
L . a = Rank a

let a be Ordinal of W; :: thesis:

A7: now :: thesis:

A8: a in On W by ZF_REFLE:7;
given A being Ordinal such that A9: a = succ A ; :: thesis:
A in a by A9, ORDINAL1:6;
then A in On W by A8, ORDINAL1:10;
then reconsider A = A as Ordinal of W by ZF_REFLE:7;
L . (succ A) = Rank (succ A) by A5;
hence ( a <> {} implies L . a = Rank a ) by A9; :: thesis:

end;

( a is limit_ordinal or ex A being Ordinal st a = succ A ) by ORDINAL1:29;
hence ( a <> {} implies L . a = Rank a ) by A4, A7; :: thesis:

end;

rng L c= W

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in rng L ; :: thesis:
then consider u being object such that
A10: u in On W and
A11: e = L . u by A1, FUNCT_1:def 3;
reconsider u = u as Ordinal of W by A10, ZF_REFLE:7;
( Rank (1-element_of W) in W & Rank u in W ) by Th31;
hence e in W by A1, A6, A10, A11; :: thesis:

end;

then reconsider L = L as Sequence of W by RELAT_1:def 19;

assume {} in rng L ; :: thesis:
then consider e being object such that
A12: e in On W and
A13: {} = L . e by A1, FUNCT_1:def 3;
reconsider e = e as Ordinal of W by A12, ZF_REFLE:7;
( ( e = {} & 1-element_of W = {{}} ) or e <> {} ) by ORDINAL3:15;
then ( ( L . e = Rank (1-element_of W) & 1-element_of W <> {} ) or ( e <> {} & L . e = Rank e ) ) by A1, A6, ZF_REFLE:7;
hence contradiction by A13, Th32; :: thesis:

end;

then reconsider L = L as DOMAIN-Sequence of W by A1, RELAT_1:def 9, ZF_REFLE:def 2;
A14: Union L = W

thus Union L c= W ; :: according to XBOOLE_0:def 10 :: thesis:
let e be object ; :: according to TARSKI:def 3 :: thesis:
A15: Union L = union (rng L) by CARD_3:def 4;
assume e in W ; :: thesis:
then A16: e in Rank (On W) by CLASSES2:50;
On W is limit_ordinal by CLASSES2:51;
then consider A being Ordinal such that
A17: A in On W and
A18: e in Rank A by A16, CLASSES1:31;
reconsider A = A as Ordinal of W by A17, ZF_REFLE:7;
( L . A = Rank A & L . A in rng L ) by A1, A6, A17, A18, CLASSES1:29, FUNCT_1:def 3;
then Rank A c= Union L by A15, ZFMISC_1:74;
hence e in Union L by A18; :: thesis:

end;

A19: 0-element_of W in On W by ZF_REFLE:7;
A20: for a, b being Ordinal of W st a in b holds
L . a c= L . b

let a, b be Ordinal of W; :: thesis:
assume A21: a in b ; :: thesis:
then A22: ( Rank a in Rank b & succ a c= b ) by CLASSES1:36, ORDINAL1:21;
A23: L . b = Rank b by A6, A21;
( L . a = Rank a or ( a = 0-element_of W & L . a = Rank (1-element_of W) & 1-element_of W = succ (0-element_of W) ) ) by A1, A19, A6;
hence L . a c= L . b by A22, A23, CLASSES1:37, ORDINAL1:def 2; :: thesis:

end;

A24: for a being Ordinal of W st a <> {} & a is limit_ordinal holds
L . a = Union (L | a)

let a be Ordinal of W; :: thesis:
assume that
A25: a <> {} and
A26: a is limit_ordinal ; :: thesis:
A27: a in On W by ZF_REFLE:7;
A28: L . a = Rank a by A4, A25, A26;
thus L . a c= Union (L | a) :: according to XBOOLE_0:def 10 :: thesis:

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in L . a ; :: thesis:
then consider B being Ordinal such that
A29: B in a and
A30: e in Rank B by A25, A26, A28, CLASSES1:31;
B in On W by A27, A29, ORDINAL1:10;
then reconsider B = B as Ordinal of W by ZF_REFLE:7;
A31: ( succ B in On W & Union (L | a) = union (rng (L | a)) ) by CARD_3:def 4, ZF_REFLE:7;
L . (succ B) = Rank (succ B) by A5;
then A32: Rank B c= L . (succ B) by CLASSES1:33;
succ B in a by A26, A29, ORDINAL1:28;
then L . (succ B) c= Union (L | a) by A1, A31, FUNCT_1:50, ZFMISC_1:74;
then Rank B c= Union (L | a) by A32;
hence e in Union (L | a) by A30; :: thesis:

end;

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in Union (L | a) ; :: thesis:
then e in union (rng (L | a)) by CARD_3:def 4;
then consider X being set such that
A33: e in X and
A34: X in rng (L | a) by TARSKI:def 4;
consider u being object such that
A35: u in dom (L | a) and
A36: X = (L | a) . u by A34, FUNCT_1:def 3;
reconsider u = u as Ordinal by A35;
A37: X = L . u by A35, A36, FUNCT_1:47;
A38: dom (L | a) c= a by RELAT_1:58;
then u in On W by A27, A35, ORDINAL1:10;
then reconsider u = u as Ordinal of W by ZF_REFLE:7;
L . u c= L . a by A20, A35, A38;
hence e in L . a by A33, A37; :: thesis:

end;

assume omega in W ; :: thesis:
then consider phi being Ordinal-Sequence of W such that
A39: ( phi is increasing & phi is continuous ) and
A40: for a being Ordinal of W st phi . a = a & {} <> a holds
L . a is_elementary_subsystem_of Union L by A20, A24, Th30;
take phi ; :: thesis:
thus ( phi is increasing & phi is continuous ) by A39; :: thesis:
let a be Ordinal of W; :: thesis:
let M be non empty set ; :: thesis:
assume that
A41: phi . a = a and
A42: {} <> a and
A43: M = Rank a ; :: thesis:
M = L . a by A6, A42, A43;
hence M is_elementary_subsystem_of W by A40, A14, A41, A42; :: thesis: