let a, b be Ordinal; :: thesis: for U being Universe st omega in U & a in U & b in U holds
b -Veblen a = ((U -Veblen) . b) . a
let U be Universe; :: thesis: ( omega in U & a in U & b in U implies b -Veblen a = ((U -Veblen) . b) . a )
assume A1: ( omega in U & a in U & b in U ) ; :: thesis: b -Veblen a = ((U -Veblen) . b) . a
set W = Tarski-Class ((b \/ a) \/ omega);
( omega in Tarski-Class ((b \/ a) \/ omega) & a in Tarski-Class ((b \/ a) \/ omega) & b in Tarski-Class ((b \/ a) \/ omega) ) by Th57, Th66;
hence b -Veblen a = ((U -Veblen) . b) . a by A1, Th64; :: thesis: verum