let a be ordinal number ; :: thesis: 0 -Veblen a = exp (omega,a)
set b = (0 \/ a) \/ omega;
set U = Tarski-Class ((0 \/ a) \/ omega);
(0 \/ a) \/ omega in Tarski-Class ((0 \/ a) \/ omega) by CLASSES1:2;
then 00: (0 \/ a) \/ omega in On (Tarski-Class ((0 \/ a) \/ omega)) by ORDINAL1:def 9;
omega in On (Tarski-Class ((0 \/ a) \/ omega)) by 00, ORDINAL1:12, XBOOLE_1:7;
then A0: omega in Tarski-Class ((0 \/ a) \/ omega) by ORDINAL1:def 9;
a in On (Tarski-Class ((0 \/ a) \/ omega)) by 00, ORDINAL1:12, XBOOLE_1:7;
then A1: a in Tarski-Class ((0 \/ a) \/ omega) by ORDINAL1:def 9;
thus 0 -Veblen a = ((Tarski-Class ((0 \/ a) \/ omega)) exp omega) . a by V
.= exp (omega,a) by A1, A0, EXP ; :: thesis: verum