let a be Ordinal; :: thesis: for U, W being Universe st omega in U & U c= W & a in U holds
(U -Veblen) . a c= (W -Veblen) . a
let U, W be Universe; :: thesis: ( omega in U & U c= W & a in U implies (U -Veblen) . a c= (W -Veblen) . a )
assume A1: ( omega in U & U c= W ) ; :: thesis: ( not a in U or (U -Veblen) . a c= (W -Veblen) . a )
then A2: On U c= On W by ORDINAL2:9;
defpred S1[ Ordinal] means ( $1 in U implies (U -Veblen) . $1 c= (W -Veblen) . $1 );
A3: ( (U -Veblen) . 0 = U exp omega & (W -Veblen) . 0 = W exp omega ) by Def15;
A4: ( dom (U exp omega) = On U & dom (W exp omega) = On W ) by FUNCT_2:def 1;
now :: thesis: for x being object st x in On U holds
(U exp omega) . x = (W exp omega) . x
let x be object ; :: thesis: ( x in On U implies (U exp omega) . x = (W exp omega) . x )
assume x in On U ; :: thesis: (U exp omega) . x = (W exp omega) . x
then reconsider a = x as Ordinal of U by ORDINAL1:def 9;
reconsider b = a as Ordinal of W by A1;
(U exp omega) . a = exp (omega,b) by A1, Def8;
hence (U exp omega) . x = (W exp omega) . x by A1, Def8; :: thesis: verum
end;
then A5: S1[ 0 ] by A2, A3, A4, GRFUNC_1:2;
A6: for b being Ordinal st S1[b] holds
S1[ succ b]
proof
let b be Ordinal; :: thesis: ( S1[b] implies S1[ succ b] )
assume A7: S1[b] ; :: thesis: S1[ succ b]
assume A8: succ b in U ; :: thesis: (U -Veblen) . (succ b) c= (W -Veblen) . (succ b)
A9: b in succ b by ORDINAL1:6;
( succ b in On U & succ b in On W ) by A1, A8, ORDINAL1:def 9;
then ( (U -Veblen) . (succ b) = criticals ((U -Veblen) . b) & (W -Veblen) . (succ b) = criticals ((W -Veblen) . b) ) by Def15;
hence (U -Veblen) . (succ b) c= (W -Veblen) . (succ b) by A7, A9, Th40, A8, ORDINAL1:10; :: thesis: verum
end;
A10: for b being Ordinal st b <> 0 & b is limit_ordinal & ( for c being Ordinal st c in b holds
S1[c] ) holds
S1[b]
proof
let b be Ordinal; :: thesis: ( b <> 0 & b is limit_ordinal & ( for c being Ordinal st c in b holds
S1[c] ) implies S1[b] )
assume that
A11: ( b <> 0 & b is limit_ordinal ) and
A12: for c being Ordinal st c in b holds
S1[c] and
A13: b in U ; :: thesis: (U -Veblen) . b c= (W -Veblen) . b
set g1 = (U -Veblen) | b;
set g2 = (W -Veblen) | b;
A14: ( b in On U & b in On W ) by A1, A13, ORDINAL1:def 9;
then A15: ( (U -Veblen) . b = criticals ((U -Veblen) | b) & (W -Veblen) . b = criticals ((W -Veblen) | b) ) by A11, Def15;
( dom (U -Veblen) = On U & dom (W -Veblen) = On W ) by Def15;
then ( b c= dom (U -Veblen) & b c= dom (W -Veblen) ) by A14, ORDINAL1:def 2;
then A16: ( dom ((U -Veblen) | b) = b & dom ((W -Veblen) | b) = b ) by RELAT_1:62;
now :: thesis: for a being Ordinal st a in dom ((U -Veblen) | b) holds
((U -Veblen) | b) . a c= ((W -Veblen) | b) . a
let a be Ordinal; :: thesis: ( a in dom ((U -Veblen) | b) implies ((U -Veblen) | b) . a c= ((W -Veblen) | b) . a )
assume A17: a in dom ((U -Veblen) | b) ; :: thesis: ((U -Veblen) | b) . a c= ((W -Veblen) | b) . a
then A18: ( ((U -Veblen) | b) . a = (U -Veblen) . a & ((W -Veblen) | b) . a = (W -Veblen) . a ) by A16, FUNCT_1:47;
a in U by A13, A16, A17, ORDINAL1:10;
hence ((U -Veblen) | b) . a c= ((W -Veblen) | b) . a by A12, A16, A17, A18; :: thesis: verum
end;
hence (U -Veblen) . b c= (W -Veblen) . b by A11, A15, A16, Th55; :: thesis: verum
end;
for b being Ordinal holds S1[b] from ORDINAL2:sch 1(A5, A6, A10);
 hence ( not a in U or (U -Veblen) . a c= (W -Veblen) . a ) ; :: thesis: verum