let n be Nat; :: thesis: for C being being_simple_closed_curve Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
X-SpanStart (C,n) = ((2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2)) + 2
let C be being_simple_closed_curve Subset of (TOP-REAL 2); :: thesis: ( n is_sufficiently_large_for C implies X-SpanStart (C,n) = ((2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2)) + 2 )
set m = ApproxIndex C;
A1: ApproxIndex C >= 1 by Th1;
assume n is_sufficiently_large_for C ; :: thesis: X-SpanStart (C,n) = ((2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2)) + 2
then A2: n >= ApproxIndex C by Def1;
(n -' (ApproxIndex C)) + ((ApproxIndex C) -' 1) = (n -' (ApproxIndex C)) + ((ApproxIndex C) - 1) by Th1, XREAL_1:233
.= ((n -' (ApproxIndex C)) + (ApproxIndex C)) - 1
.= n - 1 by A2, XREAL_1:235
.= n -' 1 by A2, A1, XREAL_1:233, XXREAL_0:2 ;
hence X-SpanStart (C,n) = ((2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart (C,(ApproxIndex C))) - 2)) + 2 by NEWTON:8; :: thesis: verum