let a be Ordinal; :: 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
A1: omega in U and
A2: 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 A2, CLASSES2:5;
then succ a in On U by ORDINAL1:def 9;
then (U -Veblen) . (succ a) = criticals f by Def15;
hence (U -Veblen) . (succ a) is normal Ordinal-Sequence of U by A1, Th44; :: thesis: verum