let L be Real; :: thesis: ( 0 < L & L < 1 implies for k being Element of NAT holds
( L to_power k <= 1 & 0 < L to_power k ) )
assume A1: ( 0 < L & L < 1 ) ; :: thesis: for k being Element of NAT holds
( L to_power k <= 1 & 0 < L to_power k )
defpred S₁[ Element of NAT ] means ( L to_power $1 <= 1 & 0 < L to_power $1 );
A2: S₁[ 0 ] by POWER:29;
A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: ( L to_power k <= 1 & 0 < L to_power k ) ; :: thesis: S₁[k + 1]
A5: L to_power (k + 1) = (L to_power k) * (L to_power 1) by A1, POWER:32
.= (L to_power k) * L by POWER:30 ;
(L to_power k) * L <= L to_power k by A1, A4, XREAL_1:155;
hence S₁[k + 1] by A1, A4, A5, XREAL_1:131, XXREAL_0:2; :: thesis: verum

end;

thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A3); :: thesis: verum