let C be compact non horizontal non vertical Subset of (TOP-REAL 2); 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; ( 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
; ( not n >= 1 or X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2 )
assume A3:
n >= 1
; 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; verum