let a be ordinal number ; :: thesis: for m, n being natural number st 1 in a & m < n holds
a |^|^ m in a |^|^ n
let m, n be natural number ; :: thesis: ( 1 in a & m < n implies a |^|^ m in a |^|^ n )
assume A0: ( 1 in a & m < n ) ; :: thesis: a |^|^ m in a |^|^ n
then m + 1 <= n by NAT_1:13;
then consider k being Nat such that
A1: n = (m + 1) + k by NAT_1:10;
defpred S1[ Nat] means a |^|^ $1 in a |^|^ ($1 + 1);
defpred S2[ Nat] means a |^|^ m in a |^|^ ((m + 1) + $1);
a |^|^ 0 = 1 by Th0;
then B0: S1[ 0 ] by A0, Th3;
B1: now
let n be natural number ; :: thesis: ( S1[n] implies S1[n + 1] )
assume S1[n] ; :: thesis: S1[n + 1]
then B2: exp a,(a |^|^ n) in exp a,(a |^|^ (n + 1)) by A0, ORDINAL4:24;
( succ n = n + 1 & succ (n + 1) = (n + 1) + 1 ) by NAT_1:39;
then ( a |^|^ (n + 1) = exp a,(a |^|^ n) & a |^|^ ((n + 1) + 1) = exp a,(a |^|^ (n + 1)) ) by Th1;
hence S1[n + 1] by B2; :: thesis: verum
end;
BB: for n being natural number holds S1[n] from NAT_1:sch 2(B0, B1);
 then A2: S2[ 0 ] ;
A3: now
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A4: S2[k] ; :: thesis: S2[k + 1]
a |^|^ ((m + 1) + k) in a |^|^ (((m + 1) + k) + 1) by BB;
hence S2[k + 1] by A4, ORDINAL1:19; :: thesis: verum
end;
for k being Nat holds S2[k] from NAT_1:sch 2(A2, A3);
 hence a |^|^ m in a |^|^ n by A1; :: thesis: verum