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 A1: ( f is special & 2 <= len f & 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 )
then 1 <= len f by XXREAL_0:2;
then consider g being FinSequence of (TOP-REAL 2) such that
A2: g is_Shortcut_of f by Th13;
A3: ( g is one-to-one & rng (PairF g) c= rng (PairF f) & g . 1 = f . 1 & g . (len g) = f . (len f) ) by A1, A2, Def3, Th14, Th15;
A4: L~ g c= L~ f by A2, Th27;
A5: rng g c= rng f by A2, Th26;
1 <= len g by A2, Th12;
then 1 < len g by A1, A3, XXREAL_0:1;
then 1 + 1 <= len g by NAT_1:13;
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, A2, A3, A4, A5, Th28; :: thesis: verum