let a be Ordinal; :: thesis: for m, n being Nat st 1 in a & m < n holds
a |^|^ m in a |^|^ n
let m, n be Nat; :: thesis: ( 1 in a & m < n implies a |^|^ m in a |^|^ n )
assume A1: ( 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
A2: 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 Th13;
then A3: S1[ 0 ] by A1, Th16;
A4: now :: thesis: for n being Nat st S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A5: S1[n] ; :: thesis: S1[n + 1]
( succ (Segm n) = Segm (n + 1) & succ (Segm (n + 1)) = Segm ((n + 1) + 1) ) by NAT_1:38;
then ( a |^|^ (n + 1) = exp (a,(a |^|^ n)) & a |^|^ ((n + 1) + 1) = exp (a,(a |^|^ (n + 1))) ) by Th14;
hence S1[n + 1] by A5, A1, ORDINAL4:24; :: thesis: verum
end;
A6: for n being Nat holds S1[n] from NAT_1:sch 2(A3, A4);
 then A7: S2[ 0 ] ;
A8: now :: thesis: for k being Nat st S2[k] holds
S2[k + 1]
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A9: S2[k] ; :: thesis: S2[k + 1]
a |^|^ ((m + 1) + k) in a |^|^ (((m + 1) + k) + 1) by A6;
hence S2[k + 1] by A9, ORDINAL1:10; :: thesis: verum
end;
for k being Nat holds S2[k] from NAT_1:sch 2(A7, A8);
 hence a |^|^ m in a |^|^ n by A2; :: thesis: verum