let a be ordinal number ; :: 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 A0: ( omega in U & U c= W ) ; :: thesis: ( not a in U or (U -Veblen) . a c= (W -Veblen) . a )
then B0: On U c= On W by ORDINAL2:9;
defpred S₁[ ordinal number ] means ( $1 in U implies (U -Veblen) . $1 c= (W -Veblen) . $1 );
A1: ( (U -Veblen) . 0 = U exp omega & (W -Veblen) . 0 = W exp omega ) by V;
A2: ( dom (U exp omega) = On U & dom (W exp omega) = On W ) by FUNCT_2:def 1;

now

let x be set ; :: 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;
a in U ;
then reconsider b = a as Ordinal of W by A0;
(U exp omega) . a = exp (omega,b) by A0, EXP;
hence (U exp omega) . x = (W exp omega) . x by A0, EXP; :: thesis: verum

end;

then 00: S₁[ 0 ] by B0, A1, A2, GRFUNC_1:2;
01: for b being ordinal number st S₁[b] holds
S₁[ succ b]

proof

let b be ordinal number ; :: thesis: ( S₁[b] implies S₁[ succ b] )
assume S2: S₁[b] ; :: thesis: S₁[ succ b]
assume S4: succ b in U ; :: thesis: (U -Veblen) . (succ b) c= (W -Veblen) . (succ b)
S5: b in succ b by ORDINAL1:6;
( succ b in On U & succ b in On W ) by A0, S4, ORDINAL1:def 9;
then ( (U -Veblen) . (succ b) = criticals ((U -Veblen) . b) & (W -Veblen) . (succ b) = criticals ((W -Veblen) . b) ) by V;
hence (U -Veblen) . (succ b) c= (W -Veblen) . (succ b) by S2, S5, Th0A, S4, ORDINAL1:10; :: thesis: verum

end;

02: for b being ordinal number st b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S₁[c] ) holds
S₁[b]

proof

let b be ordinal number ; :: thesis: ( b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S₁[c] ) implies S₁[b] )
assume that
A1: ( b <> {} & b is limit_ordinal ) and
A2: for c being ordinal number st c in b holds
S₁[c] and
A3: b in U ; :: thesis: (U -Veblen) . b c= (W -Veblen) . b
set g1 = (U -Veblen) | b;
set g2 = (W -Veblen) | b;
A5: ( b in On U & b in On W ) by A0, A3, ORDINAL1:def 9;
then A4: ( (U -Veblen) . b = criticals ((U -Veblen) | b) & (W -Veblen) . b = criticals ((W -Veblen) | b) ) by A1, V;
( dom (U -Veblen) = On U & dom (W -Veblen) = On W ) by V;
then ( b c= dom (U -Veblen) & b c= dom (W -Veblen) ) by A5, ORDINAL1:def 2;
then A6: ( dom ((U -Veblen) | b) = b & dom ((W -Veblen) | b) = b ) by RELAT_1:62;

now

let a be ordinal number ; :: thesis: ( a in dom ((U -Veblen) | b) implies ((U -Veblen) | b) . a c= ((W -Veblen) | b) . a )
assume A7: a in dom ((U -Veblen) | b) ; :: thesis: ((U -Veblen) | b) . a c= ((W -Veblen) | b) . a
then A8: ( ((U -Veblen) | b) . a = (U -Veblen) . a & ((W -Veblen) | b) . a = (W -Veblen) . a ) by A6, FUNCT_1:47;
a in U by A3, A6, A7, ORDINAL1:10;
hence ((U -Veblen) | b) . a c= ((W -Veblen) | b) . a by A2, A6, A7, A8; :: thesis: verum

end;

hence (U -Veblen) . b c= (W -Veblen) . b by A1, A4, A6, ThAC; :: thesis: verum

end;

for b being ordinal number holds S₁[b] from ORDINAL2:sch 1(00, 01, 02);
hence ( not a in U or (U -Veblen) . a c= (W -Veblen) . a ) ; :: thesis: verum