let f be FinSequence of (TOP-REAL 2); ( 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)
; 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; verum