let A be non empty set ; :: thesis: for O being Ordinal holds A c= ConsecutiveSet2 (A,O)
let O be Ordinal; :: thesis: A c= ConsecutiveSet2 (A,O)
defpred S₁[ Ordinal] means A c= ConsecutiveSet2 (A,$1);
A1: for O1 being Ordinal st S₁[O1] holds
S₁[ succ O1]

proof

let O1 be Ordinal; :: thesis: ( S₁[O1] implies S₁[ succ O1] )
ConsecutiveSet2 (A,(succ O1)) = new_set2 (ConsecutiveSet2 (A,O1)) by Th15;
then A2: ConsecutiveSet2 (A,O1) c= ConsecutiveSet2 (A,(succ O1)) by XBOOLE_1:7;
assume A c= ConsecutiveSet2 (A,O1) ; :: thesis: S₁[ succ O1]
hence S₁[ succ O1] by A2, XBOOLE_1:1; :: thesis: verum

end;

A3: for O1 being Ordinal st O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S₁[O2] ) holds
S₁[O1]

proof

deffunc H₁( Ordinal) -> set = ConsecutiveSet2 (A,$1);
let O2 be Ordinal; :: thesis: ( O2 <> 0 & O2 is limit_ordinal & ( for O2 being Ordinal st O2 in O2 holds
S₁[O2] ) implies S₁[O2] )
assume that
A4: O2 <> 0 and
A5: O2 is limit_ordinal and
for O1 being Ordinal st O1 in O2 holds
A c= ConsecutiveSet2 (A,O1) ; :: thesis: S₁[O2]
A6: {} in O2 by A4, ORDINAL3:8;
consider Ls being Sequence such that
A7: ( dom Ls = O2 & ( for O1 being Ordinal st O1 in O2 holds
Ls . O1 = H₁(O1) ) ) from ORDINAL2:sch 2();
Ls . {} = ConsecutiveSet2 (A,{}) by A4, A7, ORDINAL3:8
.= A by Th14 ;
then A8: A in rng Ls by A7, A6, FUNCT_1:def 3;
ConsecutiveSet2 (A,O2) = union (rng Ls) by A4, A5, A7, Th16;
hence S₁[O2] by A8, ZFMISC_1:74; :: thesis: verum

end;

A9: S₁[ 0 ] by Th14;
for O being Ordinal holds S₁[O] from ORDINAL2:sch 1(A9, A1, A3);
hence A c= ConsecutiveSet2 (A,O) ; :: thesis: verum