let f, g be FinSequence of (TOP-REAL 2); :: thesis: ( f is special & g is_Shortcut_of f implies g is special )
assume A1:
( f is special & g is_Shortcut_of f )
; :: thesis: g is special
for i being Nat st 1 <= i & i + 1 <= len g & not (g /. i) `1 = (g /. (i + 1)) `1 holds
(g /. i) `2 = (g /. (i + 1)) `2
proof
let i be
Nat;
:: thesis: ( 1 <= i & i + 1 <= len g & not (g /. i) `1 = (g /. (i + 1)) `1 implies (g /. i) `2 = (g /. (i + 1)) `2 )
assume A2:
( 1
<= i &
i + 1
<= len g )
;
:: thesis: ( (g /. i) `1 = (g /. (i + 1)) `1 or (g /. i) `2 = (g /. (i + 1)) `2 )
then A3:
i <= len g
by NAT_1:13;
A4:
i in NAT
by ORDINAL1:def 13;
A5:
1
<= i + 1
by A2, NAT_1:13;
A6:
rng (PairF g) c= rng (PairF f)
by A1, Th14;
A7:
i < len g
by A2, NAT_1:13;
then A8:
(PairF g) . i = [(g . i),(g . (i + 1))]
by A2, A4, Def2;
A9:
len (PairF g) = (len g) -' 1
by Def2;
A10:
i <= (len g) - 1
by A2, XREAL_1:21;
then
1
<= (len g) - 1
by A2, XXREAL_0:2;
then
(len g) -' 1
= (len g) - 1
by NAT_D:39;
then
i in dom (PairF g)
by A2, A9, A10, FINSEQ_3:27;
then
[(g . i),(g . (i + 1))] in rng (PairF g)
by A8, FUNCT_1:def 5;
then consider x being
set such that A11:
(
x in dom (PairF f) &
(PairF f) . x = [(g . i),(g . (i + 1))] )
by A6, FUNCT_1:def 5;
A12:
x in Seg (len (PairF f))
by A11, FINSEQ_1:def 3;
reconsider k =
x as
Element of
NAT by A11;
A13:
( 1
<= k &
k <= len (PairF f) )
by A12, FINSEQ_1:3;
A14:
len (PairF f) = (len f) -' 1
by Def2;
A15:
1
< len g
by A2, A7, XXREAL_0:2;
len g <= len f
by A1, Th12;
then
(len f) -' 1
= (len f) - 1
by A15, XREAL_1:235, XXREAL_0:2;
then A16:
k + 1
<= ((len f) - 1) + 1
by A13, A14, XREAL_1:8;
then A17:
k < len f
by NAT_1:13;
then
(PairF f) . k = [(f . k),(f . (k + 1))]
by A13, Def2;
then A18:
(
g . i = f . k &
g . (i + 1) = f . (k + 1) )
by A11, ZFMISC_1:33;
A19:
1
< k + 1
by A13, NAT_1:13;
A20:
g /. i = g . i
by A2, A3, FINSEQ_4:24;
A21:
g /. (i + 1) = g . (i + 1)
by A2, A5, FINSEQ_4:24;
A22:
f /. k = f . k
by A13, A17, FINSEQ_4:24;
f /. (k + 1) = f . (k + 1)
by A16, A19, FINSEQ_4:24;
hence
(
(g /. i) `1 = (g /. (i + 1)) `1 or
(g /. i) `2 = (g /. (i + 1)) `2 )
by A1, A13, A16, A18, A20, A21, A22, TOPREAL1:def 7;
:: thesis: verum
end;
hence
g is special
by TOPREAL1:def 7; :: thesis: verum