let b, a be ordinal number ; :: thesis: b -Veblen ((succ b) -Veblen a) = (succ b) -Veblen a
set U = Tarski-Class ((b \/ a) \/ omega);
A2: omega in Tarski-Class ((b \/ a) \/ omega) by Unc1;
reconsider b1 = b as Ordinal of Tarski-Class ((b \/ a) \/ omega) by LemT;
succ b1 in On (Tarski-Class ((b \/ a) \/ omega)) by ORDINAL1:def 9;
then A4: ((Tarski-Class ((b \/ a) \/ omega)) -Veblen) . (succ b) = criticals (((Tarski-Class ((b \/ a) \/ omega)) -Veblen) . b) by V;
reconsider f = ((Tarski-Class ((b \/ a) \/ omega)) -Veblen) . b1, g = ((Tarski-Class ((b \/ a) \/ omega)) -Veblen) . (succ b1) as normal Ordinal-Sequence of (Tarski-Class ((b \/ a) \/ omega)) by A2, Th23;
A1: a in Tarski-Class ((b \/ a) \/ omega) by LemT;
then A3: a in On (Tarski-Class ((b \/ a) \/ omega)) by ORDINAL1:def 9;
A5: ( dom f = On (Tarski-Class ((b \/ a) \/ omega)) & dom g = On (Tarski-Class ((b \/ a) \/ omega)) ) by FUNCT_2:def 1;
set W = Tarski-Class ((b \/ (g . a)) \/ omega);
omega in Tarski-Class ((b \/ a) \/ omega) by Unc1;
then A7: ( (succ b1) -Veblen a = g . a & b1 -Veblen (g . a) = f . (g . a) ) by A1, Th26;
then (succ b) -Veblen a is_a_fixpoint_of ((Tarski-Class ((b \/ a) \/ omega)) -Veblen) . b by A3, A4, A5, Th02;
hence b -Veblen ((succ b) -Veblen a) = (succ b) -Veblen a by A7, ABIAN:def 3; :: thesis: verum