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