let n be Nat; :: thesis: for a being non trivial Nat st n <= a holds
ex T being _Theta st Py (a,(n + 1)) = ((2 * a) |^ n) * (1 + (T * (n / a)))
let a be non trivial Nat; :: thesis: ( n <= a implies ex T being _Theta st Py (a,(n + 1)) = ((2 * a) |^ n) * (1 + (T * (n / a))) )
assume A1: n <= a ; :: thesis: ex T being _Theta st Py (a,(n + 1)) = ((2 * a) |^ n) * (1 + (T * (n / a)))

per cases ( n = 0 or n > 0 ) ;

suppose A2: n = 0 ; :: thesis: ex T being _Theta st Py (a,(n + 1)) = ((2 * a) |^ n) * (1 + (T * (n / a)))

then ( Py (a,(n + 1)) = (Px (a,0)) + ((Py (a,0)) * a) & Px (a,0) = 1 & Py (a,0) = 0 ) by HILB10_1:3, HILB10_1:6;
then ( Py (a,(n + 1)) = 1 & 1 = ((2 * a) |^ n) * (1 + (0 * (n / a))) ) by A2;
hence ex T being _Theta st Py (a,(n + 1)) = ((2 * a) |^ n) * (1 + (T * (n / a))) ; :: thesis: verum

end;

suppose A3: n > 0 ; :: thesis: ex T being _Theta st Py (a,(n + 1)) = ((2 * a) |^ n) * (1 + (T * (n / a)))

A4: - 1 is theta ;
2 * n <= 2 * a by A1, XREAL_1:64;
then 1 / (2 * a) <= 1 / (2 * n) by A3, XREAL_1:118;
then consider T being _Theta such that
A5: (1 + ((- 1) * (1 / (2 * a)))) |^ n = 1 + (((T * 2) * n) * (1 / (2 * a))) by A4, Th9;
A6: ((T * 2) * n) * (1 / (2 * a)) = T * ((2 * n) * (1 / (2 * a)))
.= T * (((2 * n) * 1) / (2 * a)) by XCMPLX_1:74
.= T * (n / a) by XCMPLX_1:91 ;
(2 * a) - 1 = ((2 * a) * 1) - ((2 * a) * (1 / (2 * a))) by XCMPLX_1:87;
then ((2 * a) - 1) |^ n = ((2 * a) * (1 - (1 / (2 * a)))) |^ n
.= ((2 * a) |^ n) * (1 + (T * (n / a))) by A6, A5, NEWTON:7 ;
then ( ((2 * a) |^ n) + (((2 * a) |^ n) * (T * (n / a))) <= Py (a,(n + 1)) & Py (a,(n + 1)) <= ((2 * a) |^ n) + 0 ) by HILB10_1:17;
then ( ((2 * a) |^ n) * (T * (n / a)) <= (Py (a,(n + 1))) - ((2 * a) |^ n) & (Py (a,(n + 1))) - ((2 * a) |^ n) <= ((2 * a) |^ n) * (0 * (n / a)) ) by XREAL_1:19, XREAL_1:20;
then ( T * (n / a) <= ((Py (a,(n + 1))) - ((2 * a) |^ n)) / ((2 * a) |^ n) & ((Py (a,(n + 1))) - ((2 * a) |^ n)) / ((2 * a) |^ n) <= 0 * (n / a) ) by XREAL_1:77;
then consider T1 being _Theta such that
A7: T1 * (n / a) = ((Py (a,(n + 1))) - ((2 * a) |^ n)) / ((2 * a) |^ n) by Th4;
take T1 ; :: thesis: Py (a,(n + 1)) = ((2 * a) |^ n) * (1 + (T1 * (n / a)))
(T1 * (n / a)) * ((2 * a) |^ n) = (Py (a,(n + 1))) - ((2 * a) |^ n) by A7, XCMPLX_1:87;
hence Py (a,(n + 1)) = ((2 * a) |^ n) * (1 + (T1 * (n / a))) ; :: thesis: verum

end;

end;