let a be ordinal number ; :: thesis: for U being Universe st omega in U & a in U & (U -Veblen) . a is normal Ordinal-Sequence of U holds
(U -Veblen) . (succ a) is normal Ordinal-Sequence of U
let U be Universe; :: thesis: ( omega in U & a in U & (U -Veblen) . a is normal Ordinal-Sequence of U implies (U -Veblen) . (succ a) is normal Ordinal-Sequence of U )
assume that
Z0: omega in U and
Z1: a in U ; :: thesis: ( not (U -Veblen) . a is normal Ordinal-Sequence of U or (U -Veblen) . (succ a) is normal Ordinal-Sequence of U )
assume (U -Veblen) . a is normal Ordinal-Sequence of U ; :: thesis: (U -Veblen) . (succ a) is normal Ordinal-Sequence of U
then reconsider f = (U -Veblen) . a as normal Ordinal-Sequence of U ;
succ a in U by Z1, CLASSES2:5;
then succ a in On U by ORDINAL1:def 9;
then (U -Veblen) . (succ a) = criticals f by V;
hence (U -Veblen) . (succ a) is normal Ordinal-Sequence of U by Z0, Th39; :: thesis: verum