let l be limit_ordinal non empty Ordinal; :: thesis: ( ( for a being ordinal number st a in l holds
1 -Veblen a = epsilon_ a ) implies 1 -Veblen l = epsilon_ l )
assume Z0: for a being ordinal number st a in l holds
1 -Veblen a = epsilon_ a ; :: thesis: 1 -Veblen l = epsilon_ l
set U = Tarski-Class (l \/ omega);
0 in l by ORDINAL3:8;
then omega c= l by ORDINAL1:def 11;
then l \/ omega = l by XBOOLE_1:12;
then A1: l in Tarski-Class (l \/ omega) by CLASSES1:2;
A2: omega in Tarski-Class (l \/ omega) by Unc1;
1-element_of (Tarski-Class (l \/ omega)) = 1 ;
then reconsider g = ((Tarski-Class (l \/ omega)) -Veblen) . 1 as normal Ordinal-Sequence of (Tarski-Class (l \/ omega)) by A2, Th23;
reconsider o = omega as non trivial Ordinal of Tarski-Class (l \/ omega) by Unc1;
set f = (Tarski-Class (l \/ omega)) exp o;
A4: g = criticals ((Tarski-Class (l \/ omega)) exp o) by Th12;
B0: dom g = On (Tarski-Class (l \/ omega)) by FUNCT_2:def 1;
then B1: l in dom g by A1, ORDINAL1:def 9;
then A5: g . l = Union (g | l) by A4, Th09
.= union (rng (g | l)) ;
l c= dom g by B1, ORDINAL1:def 2;
then B2: dom (g | l) = l by RELAT_1:62;

now

let x be set ; :: thesis: ( x in rng (g | l) implies x c= epsilon_ l )
assume x in rng (g | l) ; :: thesis: x c= epsilon_ l
then consider y being set such that
A6: ( y in dom (g | l) & x = (g | l) . y ) by FUNCT_1:def 3;
reconsider y = y as Ordinal by A6;
A7: x = g . y by A6, FUNCT_1:47;
y in dom g by B1, B2, A6, ORDINAL1:10;
then ( y in Tarski-Class (l \/ omega) & 1-element_of (Tarski-Class (l \/ omega)) in Tarski-Class (l \/ omega) ) by B0, ORDINAL1:def 9;
then x = 1 -Veblen y by A2, A7, Th26;
then x = epsilon_ y by Z0, B2, A6;
then x in epsilon_ l by B2, A6, LemE2;
hence x c= epsilon_ l by ORDINAL1:def 2; :: thesis: verum

end;

hence 1 -Veblen l c= epsilon_ l by A5, ZFMISC_1:76; :: according to XBOOLE_0:def 10 :: thesis: epsilon_ l c= 1 -Veblen l
let a be ordinal number ; :: according to ORDINAL1:def 5 :: thesis: ( not a in epsilon_ l or a in 1 -Veblen l )
assume a in epsilon_ l ; :: thesis: a in 1 -Veblen l
then consider b being ordinal number such that
A8: ( b in l & a in epsilon_ b ) by ORDINAL5:47;
epsilon_ b = 1 -Veblen b by Z0, A8;
then epsilon_ b in 1 -Veblen l by A8, Th15a;
hence a in 1 -Veblen l by A8, ORDINAL1:10; :: thesis: verum