let a be Real; :: thesis: for n being natural Number st 1 <= a & 1 <= n holds
a <= a |^ n
let n be natural Number ; :: thesis: ( 1 <= a & 1 <= n implies a <= a |^ n )
assume that
A1: 1 <= a and
A2: 1 <= n ; :: thesis: a <= a |^ n
consider m being Nat such that
A3: n = m + 1 by A2, NAT_1:6;
defpred S₁[ Nat] means a <= a |^ ($1 + 1);
A4: for m1 being Nat st S₁[m1] holds
S₁[m1 + 1]

proof

let m1 be Nat; :: thesis: ( S₁[m1] implies S₁[m1 + 1] )
assume a <= a |^ (m1 + 1) ; :: thesis: S₁[m1 + 1]
then a * 1 <= (a |^ (m1 + 1)) * a by A1, XREAL_1:66;
hence S₁[m1 + 1] by NEWTON:6; :: thesis: verum

end;

A5: S₁[ 0 ] ;
A6: for m1 being Nat holds S₁[m1] from NAT_1:sch 2(A5, A4);
thus a <= a |^ n by A3, A6; :: thesis: verum