let b be Ordinal; :: thesis: for W being Universe
for phi being normal Ordinal-Sequence of W st omega in W & b in W holds
ex a being Ordinal st
( b in a & a is_a_fixpoint_of phi )
let W be Universe; :: thesis: for phi being normal Ordinal-Sequence of W st omega in W & b in W holds
ex a being Ordinal st
( b in a & a is_a_fixpoint_of phi )
let phi be normal Ordinal-Sequence of W; :: thesis: ( omega in W & b in W implies ex a being Ordinal st
( b in a & a is_a_fixpoint_of phi ) )
assume that
A1: omega in W and
A2: b in W ; :: thesis: ex a being Ordinal st
( b in a & a is_a_fixpoint_of phi )
reconsider b1 = b as Ordinal of W by A2;
A3: dom phi = On W by FUNCT_2:def 1;
deffunc H₁( set ) -> Ordinal of W = phi . $1;
A4: for a being Ordinal st a in W holds
H₁(a) in W ;
A5: for a, b being Ordinal st a in b & b in W holds
H₁(a) in H₁(b)

proof

let a, b be Ordinal; :: thesis: ( a in b & b in W implies H₁(a) in H₁(b) )
( b in W implies b in dom phi ) by A3, ORDINAL1:def 9;
hence ( a in b & b in W implies H₁(a) in H₁(b) ) by ORDINAL2:def 12; :: thesis: verum

end;

A6: for a being Ordinal of W st not a is empty & a is limit_ordinal holds
for f being Ordinal-Sequence st dom f = a & ( for b being Ordinal st b in a holds
f . b = H₁(b) ) holds
H₁(a) is_limes_of f

proof

let a be Ordinal of W; :: thesis: ( not a is empty & a is limit_ordinal implies for f being Ordinal-Sequence st dom f = a & ( for b being Ordinal st b in a holds
f . b = H₁(b) ) holds
H₁(a) is_limes_of f )
assume A7: ( not a is empty & a is limit_ordinal ) ; :: thesis: for f being Ordinal-Sequence st dom f = a & ( for b being Ordinal st b in a holds
f . b = H₁(b) ) holds
H₁(a) is_limes_of f
let f be Ordinal-Sequence; :: thesis: ( dom f = a & ( for b being Ordinal st b in a holds
f . b = H₁(b) ) implies H₁(a) is_limes_of f )
assume that
A8: dom f = a and
A9: for b being Ordinal st b in a holds
f . b = H₁(b) ; :: thesis: H₁(a) is_limes_of f
A10: a in dom phi by A3, ORDINAL1:def 9;
then a c= dom phi by ORDINAL1:def 2;
then A11: dom (phi | a) = a by RELAT_1:62;

now :: thesis: for x being object st x in a holds
(phi | a) . x = f . x

let x be object ; :: thesis: ( x in a implies (phi | a) . x = f . x )
assume A12: x in a ; :: thesis: (phi | a) . x = f . x
reconsider xx = x as set by TARSKI:1;
thus (phi | a) . x = H₁(xx) by A12, FUNCT_1:49
.= f . x by A12, A9 ; :: thesis: verum

end;

then f = phi | a by A8, A11;
hence H₁(a) is_limes_of f by A7, A10, ORDINAL2:def 13; :: thesis: verum

end;

consider a being Ordinal of W such that
A13: ( b1 in a & H₁(a) = a ) from ORDINAL6:sch 2(A1, A4, A5, A6);
take a ; :: thesis: ( b in a & a is_a_fixpoint_of phi )
thus ( b in a & a in dom phi & a = phi . a ) by A3, A13, ORDINAL1:def 9; :: according to ABIAN:def 3 :: thesis: verum