let X be set ; :: thesis: for f being Ordinal-Sequence st f is normal & union X in dom f & not X is empty & ( for x being set st x in X holds
ex y being set st
( x c= y & y in X & y is_a_fixpoint_of f ) ) holds
union X = f . (union X)
let f be Ordinal-Sequence; :: thesis: ( f is normal & union X in dom f & not X is empty & ( for x being set st x in X holds
ex y being set st
( x c= y & y in X & y is_a_fixpoint_of f ) ) implies union X = f . (union X) )
assume that
Z0: f is normal and
Z1: ( union X in dom f & not X is empty ) and
Z2: for x being set st x in X holds
ex y being set st
( x c= y & y in X & y is_a_fixpoint_of f ) ; :: thesis: union X = f . (union X)
reconsider l = union X as Ordinal by Z1;

per cases ( ex a being ordinal number st
( a in X & ( for b being ordinal number st b in X holds
b c= a ) ) or for a being ordinal number holds
( not a in X or ex b being ordinal number st
( b in X & not b c= a ) ) ) ;

suppose ex a being ordinal number st
( a in X & ( for b being ordinal number st b in X holds
b c= a ) ) ; :: thesis: union X = f . (union X)

then consider a being ordinal number such that
A1: ( a in X & ( for b being ordinal number st b in X holds
b c= a ) ) ;

now

let x be set ; :: thesis: ( x in X implies x c= a )
assume x in X ; :: thesis: x c= a
then consider y being set such that
A3: ( x c= y & y in X & y is_a_fixpoint_of f ) by Z2;
y in dom f by A3, ABIAN:def 3;
then y c= a by A1, A3;
hence x c= a by A3, XBOOLE_1:1; :: thesis: verum

end;

then ( union X c= a & a c= union X ) by A1, ZFMISC_1:74, ZFMISC_1:76;
then A6: union X = a by XBOOLE_0:def 10;
then consider y being set such that
A4: ( union X c= y & y in X & y is_a_fixpoint_of f ) by Z2, A1;
( y in dom f & y = f . y ) by A4, ABIAN:def 3;
then y c= union X by A6, A4, A1;
then y = union X by A4, XBOOLE_0:def 10;
hence union X = f . (union X) by A4, ABIAN:def 3; :: thesis: verum

end;

suppose A3: for a being ordinal number holds
( not a in X or ex b being ordinal number st
( b in X & not b c= a ) ) ; :: thesis: union X = f . (union X)

set y0 = the Element of X;
consider x0 being set such that
B0: ( the Element of X c= x0 & x0 in X & x0 is_a_fixpoint_of f ) by Z1, Z2;
B1: x0 in dom f by B0, ABIAN:def 3;
then consider b being ordinal number such that
B2: ( b in X & b c/= x0 ) by B0, A3;
C3: x0 in b by B1, B2, EXCH1;

now

let a be ordinal number ; :: thesis: ( a in l implies succ a in l )
assume a in l ; :: thesis: succ a in l
then consider x being set such that
A4: ( a in x & x in X ) by TARSKI:def 4;
consider y being set such that
B4: ( x c= y & y in X & y is_a_fixpoint_of f ) by Z2, A4;
A5: y in dom f by B4, ABIAN:def 3;
then consider b being ordinal number such that
A6: ( b in X & b c/= y ) by A3, B4;
( succ a c= y & y in b ) by A4, B4, A5, A6, EXCH1, ORDINAL1:21;
then succ a in b by ORDINAL1:12;
hence succ a in l by A6, TARSKI:def 4; :: thesis: verum

end;

then reconsider l = l as limit_ordinal non empty Ordinal by C3, B2, ORDINAL1:28, TARSKI:def 4;
thus union X c= f . (union X) by Z1, Z0, ORDINAL4:10; :: according to XBOOLE_0:def 10 :: thesis: f . (union X) c= union X
reconsider g = f | l as increasing Ordinal-Sequence by Z0, ORDINAL4:15;
l c= dom f by Z1, ORDINAL1:def 2;
then A9: dom g = l by RELAT_1:62;
then A7: Union g is_limes_of g by ORDINAL5:6;
f . l is_limes_of g by Z0, Z1, ORDINAL2:def 13;
then A8: ( f . l = lim g & Union g = lim g ) by A7, ORDINAL2:def 10;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in f . (union X) or x in union X )
assume x in f . (union X) ; :: thesis: x in union X
then consider z being set such that
C1: ( z in dom g & x in g . z ) by A8, CARD_5:2;
consider y being set such that
C2: ( z in y & y in X ) by A9, C1, TARSKI:def 4;
consider t being set such that
C4: ( y c= t & t in X & t is_a_fixpoint_of f ) by C2, Z2;
C3: ( t in dom f & t = f . t ) by C4, ABIAN:def 3;
then reconsider z = z, t = t as Ordinal by C1;
( f . z = g . z & z in t ) by C1, C2, C4, FUNCT_1:47;
then g . z in t by Z0, C3, ORDINAL2:def 12;
then x in t by C1, ORDINAL1:10;
hence x in union X by C4, TARSKI:def 4; :: thesis: verum

end;

end;