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 S₁[ Nat] means a |^|^ $1 in a |^|^ ($1 + 1);
defpred S₂[ Nat] means a |^|^ m in a |^|^ ((m + 1) + $1);
a |^|^ 0 = 1 by Th13;
then A3: S₁[ 0 ] by A1, Th16;

A4: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A5: S₁[n] ; :: thesis: S₁[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 S₁[n + 1] by A5, A1, ORDINAL4:24; :: thesis: verum

end;

A6: for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A4);
then A7: S₂[ 0 ] ;

A8: now :: thesis: for k being Nat st S₂[k] holds
S₂[k + 1]

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A9: S₂[k] ; :: thesis: S₂[k + 1]
a |^|^ ((m + 1) + k) in a |^|^ (((m + 1) + k) + 1) by A6;
hence S₂[k + 1] by A9, ORDINAL1:10; :: thesis: verum

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(A7, A8);
hence a |^|^ m in a |^|^ n by A2; :: thesis: verum