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
A1: f is normal and
A2: ( union X in dom f & not X is empty ) and
A3: 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 A2;

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
A4: ( a in X & ( for b being ordinal number st b in X holds
b c= a ) ) ;

now :: thesis: for x being set st x in X holds
x c= a

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
A5: ( x c= y & y in X & y is_a_fixpoint_of f ) by A3;
y in dom f by A5, ABIAN:def 3;
then y c= a by A4, A5;
hence x c= a by A5, XBOOLE_1:1; :: thesis: verum

end;

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

end;

suppose A8: 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
A9: ( the Element of X c= x0 & x0 in X & x0 is_a_fixpoint_of f ) by A2, A3;
A10: x0 in dom f by A9, ABIAN:def 3;
then consider b being ordinal number such that
A11: ( b in X & b c/= x0 ) by A9, A8;
A12: x0 in b by A10, A11, Th4;

now :: thesis: for a being ordinal number st a in l holds
succ a in l

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
A13: ( a in x & x in X ) by TARSKI:def 4;
consider y being set such that
A14: ( x c= y & y in X & y is_a_fixpoint_of f ) by A3, A13;
A15: y in dom f by A14, ABIAN:def 3;
then consider b being ordinal number such that
A16: ( b in X & b c/= y ) by A8, A14;
( succ a c= y & y in b ) by A13, A14, A15, A16, Th4, ORDINAL1:21;
then succ a in b by ORDINAL1:12;
hence succ a in l by A16, TARSKI:def 4; :: thesis: verum

end;

then reconsider l = l as limit_ordinal non empty Ordinal by A12, A11, ORDINAL1:28, TARSKI:def 4;
thus union X c= f . (union X) by A2, A1, ORDINAL4:10; :: according to XBOOLE_0:def 10 :: thesis: f . (union X) c= union X
reconsider g = f | l as increasing Ordinal-Sequence by A1, ORDINAL4:15;
l c= dom f by A2, ORDINAL1:def 2;
then A17: dom g = l by RELAT_1:62;
then A18: Union g is_limes_of g by ORDINAL5:6;
f . l is_limes_of g by A1, A2, ORDINAL2:def 13;
then A19: ( f . l = lim g & Union g = lim g ) by A18, 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
A20: ( z in dom g & x in g . z ) by A19, CARD_5:2;
consider y being set such that
A21: ( z in y & y in X ) by A17, A20, TARSKI:def 4;
consider t being set such that
A22: ( y c= t & t in X & t is_a_fixpoint_of f ) by A21, A3;
A23: ( t in dom f & t = f . t ) by A22, ABIAN:def 3;
then reconsider z = z, t = t as Ordinal by A20;
( f . z = g . z & z in t ) by A20, A21, A22, FUNCT_1:47;
then g . z in t by A1, A23, ORDINAL2:def 12;
then x in t by A20, ORDINAL1:10;
hence x in union X by A22, TARSKI:def 4; :: thesis: verum

end;

end;