let a, b be ordinal number ; :: 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 number 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 number 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 number 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
Z0: l in U and
Z1: a in U and
Z2: b in l and
Z3: for c being ordinal number 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) } ;
A0: 0 in l by ORDINAL3:8;
reconsider f0 = (U -Veblen) . 0, f = (U -Veblen) . b as normal Ordinal-Sequence of U by Z2, Z3, ORDINAL3:8;
A2: ( f0 = ((U -Veblen) | l) . 0 & f = ((U -Veblen) | l) . b ) by Z2, FUNCT_1:49, ORDINAL3:8;
then A1: dom (lims ((U -Veblen) | l)) = dom f0 by LIM
.= On U by FUNCT_2:def 1 ;
A5: dom (U -Veblen) = On U by V;
l in On U by Z0, ORDINAL1:def 9;
then l c= dom (U -Veblen) by A5, ORDINAL1:def 2;
then A6: dom ((U -Veblen) | l) = l by RELAT_1:62;
then A7: (((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 Z2;

now

let c be ordinal number ; :: thesis: ( c in dom ((U -Veblen) | l) implies ((U -Veblen) | l) . c is Ordinal-Sequence of U )
assume C1: 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 A6, C1, Z3; :: thesis: verum

end;

then reconsider lg = lims ((U -Veblen) | l) as Ordinal-Sequence of U by Z0, A6, ThL1;
A9: a in On U by Z1, ORDINAL1:def 9;
then A3: lg . a = union { ((((U -Veblen) | l) . d) . a) where d is Element of dom ((U -Veblen) | l) : d in dom ((U -Veblen) | l) } by A1, LIM;
A4: ( dom f = On U & dom f0 = On U ) by FUNCT_2:def 1;
A8: 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 B0: 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
B1: ( x = (((U -Veblen) | l) . d) . a & d in dom ((U -Veblen) | l) ) ;
reconsider f2 = (U -Veblen) . d as normal Ordinal-Sequence of U by Z3, A6;
C2: f2 = ((U -Veblen) | l) . d by A6, FUNCT_1:49;
C3: dom f2 = On U by FUNCT_2:def 1;
omega c= l by A0, ORDINAL1:def 11;
then C4: ( d in U & omega in U ) by A6, Z0, CLASSES1:def 1, ORDINAL1:10;
C5: b in U by Z0, Z2, ORDINAL1:10;
C6: for c being ordinal number st c in b holds
(U -Veblen) . c is normal by Z3, Z2, 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 B2: x c= (((U -Veblen) | l) . b) . a by A9, A2, A4, B1, C2, C4, C5, C6, Th52;
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 )
B3: ( b in succ b & succ b in l ) by Z2, ORDINAL1:6, ORDINAL1:28;
then reconsider f1 = (U -Veblen) . (succ b) as normal Ordinal-Sequence of U by Z3;
B4: f1 = ((U -Veblen) | l) . (succ b) by B3, FUNCT_1:49;
succ b in U by B3, Z0, ORDINAL1:10;
then succ b in On U by ORDINAL1:def 9;
then B6: ( f1 = criticals f & dom f1 = On U ) by V, FUNCT_2:def 1;
then f . a c= y by A9, B4, Th40;
hence x c= y by B2, A2, XBOOLE_1:1; :: 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 A6, B3; :: thesis: y is_a_fixpoint_of f
thus y is_a_fixpoint_of f by A9, B4, B6, Th02; :: thesis: verum

end;

suppose C1: 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 B0; :: thesis: y is_a_fixpoint_of f
thus y is_a_fixpoint_of f by A9, B1, C1, C2, C3, C4, Th51; :: thesis: verum

end;

end;

end;

thus (lims ((U -Veblen) | l)) . a in dom ((U -Veblen) . b) by A3, A4, 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 A3, A7, A8, Th08a; :: thesis: verum