let a, b be Ordinal; :: thesis: b -Veblen ((succ b) -Veblen a) = (succ b) -Veblen a
set U = Tarski-Class ((b \/ a) \/ omega);
A1: omega in Tarski-Class ((b \/ a) \/ omega) by Th57;
reconsider b1 = b as Ordinal of Tarski-Class ((b \/ a) \/ omega) by Th66;
succ b1 in On (Tarski-Class ((b \/ a) \/ omega)) by ORDINAL1:def 9;
then A2: ((Tarski-Class ((b \/ a) \/ omega)) -Veblen) . (succ b) = criticals (((Tarski-Class ((b \/ a) \/ omega)) -Veblen) . b) by Def15;
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 A1, Th62;
A3: a in Tarski-Class ((b \/ a) \/ omega) by Th66;
then A4: 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 Th57;
then A6: ( (succ b1) -Veblen a = g . a & b1 -Veblen (g . a) = f . (g . a) ) by A3, Th67;
then (succ b) -Veblen a is_a_fixpoint_of ((Tarski-Class ((b \/ a) \/ omega)) -Veblen) . b by A4, A2, A5, Th29;
hence b -Veblen ((succ b) -Veblen a) = (succ b) -Veblen a by A6; :: thesis: verum