let a be real number ; :: 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 A1: ( 1 <= a & 1 <= n ) ; :: thesis: a <= a |^ n
then consider m being Nat such that
A2: n = m + 1 by NAT_1:6;
A3: m in NAT by ORDINAL1:def 13;
defpred S₁[ Element of NAT ] means a <= a |^ ($1 + 1);
a <= 1 * a ;
then a <= ((a GeoSeq ) . 0 ) * a by Th4;
then a <= (a |^ 0 ) * a by Def1;
then A4: S₁[ 0 ] by NEWTON:11;
A5: for m1 being Element of NAT st S₁[m1] holds
S₁[m1 + 1]

proof

let m1 be Element of NAT ; :: thesis: ( S₁[m1] implies S₁[m1 + 1] )
assume A6: a <= a |^ (m1 + 1) ; :: thesis: S₁[m1 + 1]
a * 1 <= (a |^ (m1 + 1)) * a by A1, A6, XREAL_1:68;
hence S₁[m1 + 1] by NEWTON:11; :: thesis: verum

end;

for m1 being Element of NAT holds S₁[m1] from NAT_1:sch 1(A4, A5);
hence a <= a |^ n by A2, A3; :: thesis: verum