let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is special & 2 <= len f & f . 1 <> f . (len f) implies ex g being FinSequence of (TOP-REAL 2) st

( 2 <= len g & g is special & g is one-to-one & L~ g c= L~ f & f . 1 = g . 1 & f . (len f) = g . (len g) & rng g c= rng f ) )

assume that

A1: f is special and

A2: 2 <= len f and

A3: f . 1 <> f . (len f) ; :: thesis: ex g being FinSequence of (TOP-REAL 2) st

( 2 <= len g & g is special & g is one-to-one & L~ g c= L~ f & f . 1 = g . 1 & f . (len f) = g . (len g) & rng g c= rng f )

consider g being FinSequence of (TOP-REAL 2) such that

A4: g is_Shortcut_of f by A2, Th9, XXREAL_0:2;

A5: ( g . 1 = f . 1 & g . (len g) = f . (len f) ) by A4;

1 <= len g by A4, Th8;

then 1 < len g by A3, A5, XXREAL_0:1;

then A6: 1 + 1 <= len g by NAT_1:13;

A7: ( L~ g c= L~ f & rng g c= rng f ) by A4, Th22, Th23;

g is one-to-one by A3, A4, Th11;

hence ex g being FinSequence of (TOP-REAL 2) st

( 2 <= len g & g is special & g is one-to-one & L~ g c= L~ f & f . 1 = g . 1 & f . (len f) = g . (len g) & rng g c= rng f ) by A1, A4, A7, A6, Th24; :: thesis: verum

( 2 <= len g & g is special & g is one-to-one & L~ g c= L~ f & f . 1 = g . 1 & f . (len f) = g . (len g) & rng g c= rng f ) )

assume that

A1: f is special and

A2: 2 <= len f and

A3: f . 1 <> f . (len f) ; :: thesis: ex g being FinSequence of (TOP-REAL 2) st

( 2 <= len g & g is special & g is one-to-one & L~ g c= L~ f & f . 1 = g . 1 & f . (len f) = g . (len g) & rng g c= rng f )

consider g being FinSequence of (TOP-REAL 2) such that

A4: g is_Shortcut_of f by A2, Th9, XXREAL_0:2;

A5: ( g . 1 = f . 1 & g . (len g) = f . (len f) ) by A4;

1 <= len g by A4, Th8;

then 1 < len g by A3, A5, XXREAL_0:1;

then A6: 1 + 1 <= len g by NAT_1:13;

A7: ( L~ g c= L~ f & rng g c= rng f ) by A4, Th22, Th23;

g is one-to-one by A3, A4, Th11;

hence ex g being FinSequence of (TOP-REAL 2) st

( 2 <= len g & g is special & g is one-to-one & L~ g c= L~ f & f . 1 = g . 1 & f . (len f) = g . (len g) & rng g c= rng f ) by A1, A4, A7, A6, Th24; :: thesis: verum