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