for G being Graph
for n being Nat
for p being cyclic Path of G st n in dom p holds
ex p9 being cyclic Path of G st
( p9 . 1 = p . n & len p9 = len p & rng p9 = rng p )