let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n, m being Nat st m >= n & n >= 1 holds
X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2
let n, m be Nat; :: thesis: ( m >= n & n >= 1 implies X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2 )
A1: X-SpanStart (C,n) = (2 |^ (n -' 1)) + 2 by JORDAN1H:def 2;
assume A2: m >= n ; :: thesis: ( not n >= 1 or X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2 )
assume A3: n >= 1 ; :: thesis: X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2
then (m -' n) + (n -' 1) = (m -' n) + (n - 1) by XREAL_1:233
.= ((m -' n) + n) - 1
.= m - 1 by A2, XREAL_1:235
.= m -' 1 by A2, A3, XREAL_1:233, XXREAL_0:2 ;
then 2 |^ (m -' 1) = (2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2) by A1, NEWTON:8;
hence X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2 by JORDAN1H:def 2; :: thesis: verum