theorem Th21: :: JGRAPH_1:21

for f, g being 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) )