let b, c, a be ordinal number ; :: thesis: ( b in c implies b -Veblen (c -Veblen a) = c -Veblen a )
assume Z0: b in c ; :: thesis: b -Veblen (c -Veblen a) = c -Veblen a
set U = Tarski-Class ((c \/ a) \/ omega);
A0: omega in Tarski-Class ((c \/ a) \/ omega) by Unc1;
A1: ( a in Tarski-Class ((c \/ a) \/ omega) & c in Tarski-Class ((c \/ a) \/ omega) ) by LemT;
then A2: b in Tarski-Class ((c \/ a) \/ omega) by Z0, 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 A0, LemT, Th23;
dom g = On (Tarski-Class ((c \/ a) \/ omega)) by FUNCT_2:def 1;
then a in dom g by A1, ORDINAL1:def 9;
then g . a is_a_fixpoint_of f by Z0, A0, LemT, Th51;
then g . a = f . (g . a) by ABIAN:def 3;
hence b -Veblen (c -Veblen a) = c -Veblen a by A0, A2, Th26; :: thesis: verum