let U be uncountable Universe; :: thesis: (U -Veblen) . 1 = criticals (U exp omega)
set o = succ (0-element_of U);
succ (0-element_of U) in On U by ORDINAL1:def 9;
then (U -Veblen) . 1 = criticals ((U -Veblen) . 0) by Def15;
hence (U -Veblen) . 1 = criticals (U exp omega) by Def15; :: thesis: verum