let n be Element of 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 i1 = X-SpanStart C,n;
set m = ApproxIndex C;
assume n is_sufficiently_large_for C ; :: thesis: X-SpanStart C,n = ((2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart C,(ApproxIndex C)) - 2)) + 2
then A1: n >= ApproxIndex C by Def1;
A2: ApproxIndex C >= 1 by Th1;
(n -' (ApproxIndex C)) + ((ApproxIndex C) -' 1) = (n -' (ApproxIndex C)) + ((ApproxIndex C) - 1) by Th1, XREAL_1:235
.= ((n -' (ApproxIndex C)) + (ApproxIndex C)) - 1
.= n - 1 by A1, XREAL_1:237
.= n -' 1 by A1, A2, XREAL_1:235, XXREAL_0:2 ;
hence X-SpanStart C,n = ((2 |^ (n -' (ApproxIndex C))) * ((X-SpanStart C,(ApproxIndex C)) - 2)) + 2 by NEWTON:13; :: thesis: verum