let a, b be Ordinal; :: thesis: for l being limit_ordinal non empty Ordinal
for U being Universe st l in U & a in U & b in l & ( for c being Ordinal st c in l holds
(U -Veblen) . c is normal Ordinal-Sequence of U ) holds
(lims ((U -Veblen) | l)) . a is_a_fixpoint_of (U -Veblen) . b
let l be limit_ordinal non empty Ordinal; :: thesis: for U being Universe st l in U & a in U & b in l & ( for c being Ordinal st c in l holds
(U -Veblen) . c is normal Ordinal-Sequence of U ) holds
(lims ((U -Veblen) | l)) . a is_a_fixpoint_of (U -Veblen) . b
let U be Universe; :: thesis: ( l in U & a in U & b in l & ( for c being Ordinal st c in l holds
(U -Veblen) . c is normal Ordinal-Sequence of U ) implies (lims ((U -Veblen) | l)) . a is_a_fixpoint_of (U -Veblen) . b )
assume that
A1: l in U and
A2: a in U and
A3: b in l and
A4: for c being Ordinal st c in l holds
(U -Veblen) . c is normal Ordinal-Sequence of U ; :: thesis: (lims ((U -Veblen) | l)) . a is_a_fixpoint_of (U -Veblen) . b
set F = U -Veblen ;
set g = (U -Veblen) | l;
set X = { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } ;
set u = union { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } ;
A5: 0 in l by ORDINAL3:8;
reconsider f0 = (U -Veblen) . 0, f = (U -Veblen) . b as normal Ordinal-Sequence of U by A3, A4, ORDINAL3:8;
A6: ( f0 = ((U -Veblen) | l) . 0 & f = ((U -Veblen) | l) . b ) by A3, FUNCT_1:49, ORDINAL3:8;
then A7: dom (lims ((U -Veblen) | l)) = dom f0 by Def12
.= On U by FUNCT_2:def 1 ;
A8: dom (U -Veblen) = On U by Def15;
l in On U by A1, ORDINAL1:def 9;
then l c= dom (U -Veblen) by A8, ORDINAL1:def 2;
then A9: dom ((U -Veblen) | l) = l by RELAT_1:62;
then A10: (((U -Veblen) | l) . b) . a in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } by A3;

now :: thesis: for c being Ordinal st c in dom ((U -Veblen) | l) holds
((U -Veblen) | l) . c is Ordinal-Sequence of U

let c be Ordinal; :: thesis: ( c in dom ((U -Veblen) | l) implies ((U -Veblen) | l) . c is Ordinal-Sequence of U )
assume A11: c in dom ((U -Veblen) | l) ; :: thesis: ((U -Veblen) | l) . c is Ordinal-Sequence of U
then ((U -Veblen) | l) . c = (U -Veblen) . c by FUNCT_1:47;
hence ((U -Veblen) | l) . c is Ordinal-Sequence of U by A9, A11, A4; :: thesis: verum

end;

then reconsider lg = lims ((U -Veblen) | l) as Ordinal-Sequence of U by A1, A9, Th56;
A12: a in On U by A2, ORDINAL1:def 9;
then A13: lg . a = union { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } by A7, Def12;
A14: ( dom f = On U & dom f0 = On U ) by FUNCT_2:def 1;
A15: for x being set st x in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } holds
ex y being set st
( x c= y & y in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } & y is_a_fixpoint_of f )

proof

let x be set ; :: thesis: ( x in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } implies ex y being set st
( x c= y & y in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } & y is_a_fixpoint_of f ) )
assume A16: x in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } ; :: thesis: ex y being set st
( x c= y & y in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } & y is_a_fixpoint_of f )
then consider d being Element of dom ((U -Veblen) | l) such that
A17: ( x = (((U -Veblen) | l) . d) . a & d in dom ((U -Veblen) | l) ) ;
reconsider f2 = (U -Veblen) . d as normal Ordinal-Sequence of U by A4, A9;
A18: f2 = ((U -Veblen) | l) . d by A9, FUNCT_1:49;
A19: dom f2 = On U by FUNCT_2:def 1;
omega c= l by A5, ORDINAL1:def 11;
then A20: ( d in U & omega in U ) by A9, A1, CLASSES1:def 1, ORDINAL1:10;
A21: b in U by A1, A3, ORDINAL1:10;
A22: for c being Ordinal st c in b holds
(U -Veblen) . c is normal by A4, A3, ORDINAL1:10;

per cases ( d c= b or b in d ) by ORDINAL1:16;

suppose d c= b ; :: thesis: ex y being set st
( x c= y & y in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } & y is_a_fixpoint_of f )

then A23: x c= (((U -Veblen) | l) . b) . a by A12, A6, A14, A17, A18, A20, A21, A22, Th60;
take y = (((U -Veblen) | l) . (succ b)) . a; :: thesis: ( x c= y & y in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } & y is_a_fixpoint_of f )
A24: ( b in succ b & succ b in l ) by A3, ORDINAL1:6, ORDINAL1:28;
then reconsider f1 = (U -Veblen) . (succ b) as normal Ordinal-Sequence of U by A4;
A25: f1 = ((U -Veblen) | l) . (succ b) by A24, FUNCT_1:49;
succ b in U by A24, A1, ORDINAL1:10;
then succ b in On U by ORDINAL1:def 9;
then A26: ( f1 = criticals f & dom f1 = On U ) by Def15, FUNCT_2:def 1;
then f . a c= y by A12, A25, Th45;
hence x c= y by A23, A6; :: thesis: ( y in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } & y is_a_fixpoint_of f )
thus y in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } by A9, A24; :: thesis: y is_a_fixpoint_of f
thus y is_a_fixpoint_of f by A12, A25, A26, Th29; :: thesis: verum

end;

suppose A27: b in d ; :: thesis: ex y being set st
( x c= y & y in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } & y is_a_fixpoint_of f )

take y = x; :: thesis: ( x c= y & y in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } & y is_a_fixpoint_of f )
thus ( x c= y & y in { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } ) by A16; :: thesis: y is_a_fixpoint_of f
thus y is_a_fixpoint_of f by A12, A17, A27, A18, A19, A20, Th58; :: thesis: verum

end;

end;

end;

thus (lims ((U -Veblen) | l)) . a in dom ((U -Veblen) . b) by A13, A14, ORDINAL1:def 9; :: according to ABIAN:def 3 :: thesis: (lims ((U -Veblen) | l)) . a = ((U -Veblen) . b) . ((lims ((U -Veblen) | l)) . a)
hence (lims ((U -Veblen) | l)) . a = ((U -Veblen) . b) . ((lims ((U -Veblen) | l)) . a) by A13, A10, A15, Th36; :: thesis: verum