let a be Ordinal; :: 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 A1: (0 \/ a) \/ omega in On (Tarski-Class ((0 \/ a) \/ omega)) by ORDINAL1:def 9;
omega in On (Tarski-Class ((0 \/ a) \/ omega)) by A1, ORDINAL1:12, XBOOLE_1:7;
then A2: omega in Tarski-Class ((0 \/ a) \/ omega) by ORDINAL1:def 9;
a in On (Tarski-Class ((0 \/ a) \/ omega)) by A1, ORDINAL1:12, XBOOLE_1:7;
then A3: a in Tarski-Class ((0 \/ a) \/ omega) by ORDINAL1:def 9;
thus 0 -Veblen a = ((Tarski-Class ((0 \/ a) \/ omega)) exp omega) . a by Def15
.= exp (omega,a) by A3, A2, Def8 ; :: thesis: verum