let f, g be FinSequence of (TOP-REAL 2); ( f is special & g is_Shortcut_of f implies g is special )
assume that
A1:
f is special
and
A2:
g is_Shortcut_of f
; 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
A3:
len g <= len f
by A2, Th8;
A4:
len (PairF g) = (len g) -' 1
by Def2;
let i be
Nat;
( 1 <= i & i + 1 <= len g & not (g /. i) `1 = (g /. (i + 1)) `1 implies (g /. i) `2 = (g /. (i + 1)) `2 )
assume that A5:
1
<= i
and A6:
i + 1
<= len g
;
( (g /. i) `1 = (g /. (i + 1)) `1 or (g /. i) `2 = (g /. (i + 1)) `2 )
i <= len g
by A6, NAT_1:13;
then A7:
g /. i = g . i
by A5, FINSEQ_4:15;
A8:
i < len g
by A6, NAT_1:13;
then
1
< len g
by A5, XXREAL_0:2;
then A9:
(len f) -' 1
= (len f) - 1
by A3, XREAL_1:233, XXREAL_0:2;
A10:
i <= (len g) - 1
by A6, XREAL_1:19;
then
1
<= (len g) - 1
by A5, XXREAL_0:2;
then
(len g) -' 1
= (len g) - 1
by NAT_D:39;
then A11:
i in dom (PairF g)
by A5, A4, A10, FINSEQ_3:25;
(PairF g) . i = [(g . i),(g . (i + 1))]
by A5, A8, Def2;
then A12:
[(g . i),(g . (i + 1))] in rng (PairF g)
by A11, FUNCT_1:def 3;
rng (PairF g) c= rng (PairF f)
by A2, Th10;
then consider x being
object such that A13:
x in dom (PairF f)
and A14:
(PairF f) . x = [(g . i),(g . (i + 1))]
by A12, FUNCT_1:def 3;
reconsider k =
x as
Element of
NAT by A13;
A15:
x in Seg (len (PairF f))
by A13, FINSEQ_1:def 3;
then A16:
1
<= k
by FINSEQ_1:1;
1
<= i + 1
by A5, NAT_1:13;
then A17:
g /. (i + 1) = g . (i + 1)
by A6, FINSEQ_4:15;
A18:
len (PairF f) = (len f) -' 1
by Def2;
k <= len (PairF f)
by A15, FINSEQ_1:1;
then A19:
k + 1
<= ((len f) - 1) + 1
by A18, A9, XREAL_1:6;
then A20:
k < len f
by NAT_1:13;
then
(PairF f) . k = [(f . k),(f . (k + 1))]
by A16, Def2;
then A21:
(
g . i = f . k &
g . (i + 1) = f . (k + 1) )
by A14, XTUPLE_0:1;
1
< k + 1
by A16, NAT_1:13;
then A22:
f /. (k + 1) = f . (k + 1)
by A19, FINSEQ_4:15;
f /. k = f . k
by A16, A20, FINSEQ_4:15;
hence
(
(g /. i) `1 = (g /. (i + 1)) `1 or
(g /. i) `2 = (g /. (i + 1)) `2 )
by A1, A16, A19, A21, A7, A17, A22, TOPREAL1:def 5;
verum
end;
hence
g is special
by TOPREAL1:def 5; verum