let G be Graph; :: thesis: 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 )
let n be Nat; :: thesis: 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 )
let p be cyclic Path of G; :: thesis: ( n in dom p implies ex p9 being cyclic Path of G st
( p9 . 1 = p . n & len p9 = len p & rng p9 = rng p ) )
assume A1: n in dom p ; :: thesis: ex p9 being cyclic Path of G st
( p9 . 1 = p . n & len p9 = len p & rng p9 = rng p )
then A2: 1 <= n by FINSEQ_3:25;
per cases ( n = 1 or 1 < n ) by A2, XXREAL_0:1;
suppose A3: n = 1 ; :: thesis: ex p9 being cyclic Path of G st
( p9 . 1 = p . n & len p9 = len p & rng p9 = 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 p9 being cyclic Path of G st
( p9 . 1 = p . n & len p9 = len p & rng p9 = rng p )
then 1 + 1 <= n by NAT_1:13;
then consider n1 being Nat such that
1 <= n1 and
n1 < n and
A4: n = n1 + 1 by FINSEQ_6:127;
reconsider r = ((n,(len p)) -cut p) ^ ((1,n1) -cut p) as cyclic Path of G by A4, Th8;
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, Th9; :: thesis: verum
end;
end;