let a, b, c be Ordinal; :: thesis: ( b in c implies b -Veblen (c -Veblen a) = c -Veblen a )
assume A1: b in c ; :: thesis: b -Veblen (c -Veblen a) = c -Veblen a
set U = Tarski-Class ((c \/ a) \/ omega);
A2: omega in Tarski-Class ((c \/ a) \/ omega) by Th57;
A3: ( a in Tarski-Class ((c \/ a) \/ omega) & c in Tarski-Class ((c \/ a) \/ omega) ) by Th66;
then A4: b in Tarski-Class ((c \/ a) \/ omega) by A1, ORDINAL1:10;
then reconsider f = ((Tarski-Class ((c \/ a) \/ omega)) -Veblen) . b, g = ((Tarski-Class ((c \/ a) \/ omega)) -Veblen) . c as normal Ordinal-Sequence of (Tarski-Class ((c \/ a) \/ omega)) by A2, Th66, Th62;
dom g = On (Tarski-Class ((c \/ a) \/ omega)) by FUNCT_2:def 1;
then a in dom g by A3, ORDINAL1:def 9;
then g . a is_a_fixpoint_of f by A1, A2, Th66, Th58;
then g . a = f . (g . a) ;
hence b -Veblen (c -Veblen a) = c -Veblen a by A2, A4, Th67; :: thesis: verum