let a, b be Ordinal; for U, W being Universe st omega in U & a in U & b in U & omega in W & a in W & b in W holds
((U -Veblen) . b) . a = ((W -Veblen) . b) . a
let U, W be Universe; ( omega in U & a in U & b in U & omega in W & a in W & b in W implies ((U -Veblen) . b) . a = ((W -Veblen) . b) . a )
assume A1:
( omega in U & a in U & b in U & omega in W & a in W & b in W )
; ((U -Veblen) . b) . a = ((W -Veblen) . b) . a
then A2:
( a in On U & a in On W )
by ORDINAL1:def 9;
( (W -Veblen) . b is Ordinal-Sequence of W & (U -Veblen) . b is Ordinal-Sequence of U )
by A1, Th62;
then A3:
( dom ((U -Veblen) . b) = On U & dom ((W -Veblen) . b) = On W )
by FUNCT_2:def 1;
( U c= W or W in U )
by CLASSES2:53;
then
( U c= W or W c= U )
by ORDINAL1:def 2;
then
( (U -Veblen) . b c= (W -Veblen) . b or (W -Veblen) . b c= (U -Veblen) . b )
by A1, Th63;
hence
((U -Veblen) . b) . a = ((W -Veblen) . b) . a
by A2, A3, GRFUNC_1:2; verum