let f, g be FinSequence of (TOP-REAL 2); :: thesis: for i being Element of 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 Element of NAT ; :: thesis: ( 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 & i + 1 <= len g ) ; :: thesis: 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) )
A3: i <= len g by A2, NAT_1:13;
A4: 1 <= i + 1 by A2, NAT_1:13;
A5: rng (PairF g) c= rng (PairF f) by A1, Th14;
A6: i < len g by A2, NAT_1:13;
then A7: (PairF g) . i = [(g . i),(g . (i + 1))] by A2, Def2;
A8: len (PairF g) = (len g) -' 1 by Def2;
A9: 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, A8, A9, FINSEQ_3:27;
then [(g . i),(g . (i + 1))] in rng (PairF g) by A7, FUNCT_1:def 5;
then consider x being set such that
A10: ( x in dom (PairF f) & (PairF f) . x = [(g . i),(g . (i + 1))] ) by A5, FUNCT_1:def 5;
A11: x in Seg (len (PairF f)) by A10, FINSEQ_1:def 3;
reconsider k = x as Element of NAT by A10;
A12: ( 1 <= k & k <= len (PairF f) ) by A11, FINSEQ_1:3;
A13: len (PairF f) = (len f) -' 1 by Def2;
A14: 1 < len g by A2, A6, XXREAL_0:2;
len g <= len f by A1, Th12;
then (len f) -' 1 = (len f) - 1 by A14, XREAL_1:235, XXREAL_0:2;
then A15: k + 1 <= ((len f) - 1) + 1 by A12, A13, XREAL_1:8;
then A16: k < len f by NAT_1:13;
then [(g . i),(g . (i + 1))] = [(f . k),(f . (k + 1))] by A10, A12, Def2;
then A17: ( g . i = f . k & g . (i + 1) = f . (k + 1) ) by ZFMISC_1:33;
A18: 1 < k + 1 by A12, NAT_1:13;
A19: g /. i = g . i by A2, A3, FINSEQ_4:24;
A20: g /. (i + 1) = g . (i + 1) by A2, A4, FINSEQ_4:24;
A21: f /. k = f . k by A12, A16, FINSEQ_4:24;
f /. (k + 1) = f . (k + 1) by A15, A18, FINSEQ_4:24;
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 A12, A15, A17, A19, A20, A21; :: thesis: verum