let a, b be ordinal number ; :: thesis: for n being natural number st a in b holds
n *^ (exp omega ,a) in exp omega ,b
let n be natural number ; :: thesis: ( a in b implies n *^ (exp omega ,a) in exp omega ,b )
assume a in b ; :: thesis: n *^ (exp omega ,a) in exp omega ,b
then succ a c= b by ORDINAL1:33;
then A1: exp omega ,(succ a) c= exp omega ,b by ORDINAL4:27;
A2: exp omega ,(succ a) = omega *^ (exp omega ,a) by ORDINAL2:61;
n in omega by ORDINAL1:def 13;
then n *^ (exp omega ,a) in omega *^ (exp omega ,a) by ORDINAL4:22, ORDINAL3:22;
hence n *^ (exp omega ,a) in exp omega ,b by A1, A2; :: thesis: verum