let G be Graph; :: thesis: for n being Element of NAT
for p being cyclic Path of G st n in dom p holds
ex p' being cyclic Path of G st
( p' . 1 = p . n & len p' = len p & rng p' = rng p )
let n be Element of NAT ; :: thesis: for p being cyclic Path of G st n in dom p holds
ex p' being cyclic Path of G st
( p' . 1 = p . n & len p' = len p & rng p' = rng p )
let p be cyclic Path of G; :: thesis: ( n in dom p implies ex p' being cyclic Path of G st
( p' . 1 = p . n & len p' = len p & rng p' = rng p ) )
assume A1: n in dom p ; :: thesis: ex p' being cyclic Path of G st
( p' . 1 = p . n & len p' = len p & rng p' = rng p )
then A2: ( 1 <= n & n <= len p ) by FINSEQ_3:27;

per cases ( n = 1 or 1 < n ) by A2, XXREAL_0:1;

suppose A3: n = 1 ; :: thesis: ex p' being cyclic Path of G st
( p' . 1 = p . n & len p' = len p & rng p' = rng p )

take p ; :: thesis: ( p . 1 = p . n & len p = len p & rng p = rng p )
thus ( p . 1 = p . n & len p = len p & rng p = rng p ) by A3; :: thesis: verum

end;

suppose 1 < n ; :: thesis: ex p' being cyclic Path of G st
( p' . 1 = p . n & len p' = len p & rng p' = rng p )

then 1 + 1 <= n by NAT_1:13;
then consider n1 being Element of NAT such that
A4: ( 1 <= n1 & n1 < n & n = n1 + 1 ) by GRAPH_2:1;
reconsider r = (n,(len p) -cut p) ^ (1,n1 -cut p) as cyclic Path of G by A4, Th13;
take r ; :: thesis: ( r . 1 = p . n & len r = len p & rng r = rng p )
thus ( r . 1 = p . n & len r = len p & rng r = rng p ) by A1, A4, Th14; :: thesis: verum

end;

end;