let G be Graph; for m being Nat
for p being cyclic Path of G holds (((m + 1),(len p)) -cut p) ^ ((1,m) -cut p) is cyclic Path of G
let m be Nat; for p being cyclic Path of G holds (((m + 1),(len p)) -cut p) ^ ((1,m) -cut p) is cyclic Path of G
let p be cyclic Path of G; (((m + 1),(len p)) -cut p) ^ ((1,m) -cut p) is cyclic Path of G
per cases
( m = 0 or ( 1 <= m & len p = m ) or ( 1 <= m & len p < m ) or ( 1 <= m & m < len p ) )
by NAT_1:14, XXREAL_0:1;
suppose A4:
( 1
<= m &
len p < m )
;
(((m + 1),(len p)) -cut p) ^ ((1,m) -cut p) is cyclic Path of G
m <= m + 1
by NAT_1:11;
then
len p < m + 1
by A4, XXREAL_0:2;
then A5:
(
(m + 1),
(len p))
-cut p = {}
by FINSEQ_6:def 4;
(1,
m)
-cut p = {}
by A4, FINSEQ_6:def 4;
then
(((m + 1),(len p)) -cut p) ^ ((1,m) -cut p) = {}
by A5, FINSEQ_1:34;
hence
(((m + 1),(len p)) -cut p) ^ ((1,m) -cut p) is
cyclic Path of
G
by Th7, GRAPH_1:14;
verum end; suppose A6:
( 1
<= m &
m < len p )
;
(((m + 1),(len p)) -cut p) ^ ((1,m) -cut p) is cyclic Path of Gset n1 =
m;
set n =
m + 1;
A7:
1
<= m + 1
by A6, NAT_1:13;
reconsider r1 = (1,
m)
-cut p,
r2 = (
(m + 1),
(len p))
-cut p as
Path of
G by Th5;
consider vs being
FinSequence of the
carrier of
G such that A8:
vs is_vertex_seq_of p
by GRAPH_2:33;
reconsider vs1 = (1,
(m + 1))
-cut vs,
vs2 = (
(m + 1),
(len vs))
-cut vs as
FinSequence of the
carrier of
G ;
A9:
m + 1
<= len p
by A6, NAT_1:13;
A10:
len vs = (len p) + 1
by A8;
A11:
vs2 is_vertex_seq_of r2
by A7, A9, A8, GRAPH_2:42;
len p <= (len p) + 1
by NAT_1:11;
then A12:
m + 1
<= len vs
by A9, A10, XXREAL_0:2;
then A13:
m + 1
< (len vs) + 1
by NAT_1:13;
(len vs1) + 1
= (m + 1) + 1
by A7, A12, FINSEQ_6:def 4;
then A14:
1
< len vs1
by A6, NAT_1:13;
A15:
vs1 is_vertex_seq_of r1
by A6, A8, GRAPH_2:42;
len vs <= (len vs) + 1
by NAT_1:11;
then
m + 1
<= (len vs) + 1
by A12, XXREAL_0:2;
then
(len vs2) + (m + 1) = (len vs) + 1
by A7, Lm1;
then
1
+ (m + 1) <= (len vs2) + (m + 1)
by A13, NAT_1:13;
then A16:
1
<= len vs2
by XREAL_1:6;
reconsider vs9 =
vs2 ^' vs1 as
FinSequence of the
carrier of
G ;
set r =
r2 ^ r1;
A17:
vs . (len vs) = vs . 1
by A8, MSSCYC_1:6;
A18:
(
vs1 . 1
= vs . 1 &
vs2 . (len vs2) = vs . (len vs) )
by A7, A12, FINSEQ_6:138;
then reconsider r =
r2 ^ r1 as
Chain of
G by A17, A15, A11, GRAPH_2:43;
A19:
vs9 is_vertex_seq_of r
by A17, A15, A11, A18, GRAPH_2:44;
p = r1 ^ r2
by A6, FINSEQ_6:135;
then
rng r1 misses rng r2
by FINSEQ_3:91;
then reconsider r =
r as
Path of
G by A17, A15, A11, A18, Th6;
(
vs1 . (len vs1) = vs . (m + 1) &
vs2 . 1
= vs . (m + 1) )
by A7, A12, FINSEQ_6:138;
then vs9 . 1 =
vs1 . (len vs1)
by A16, FINSEQ_6:140
.=
vs9 . (len vs9)
by A14, FINSEQ_6:142
;
then
r is
cyclic Path of
G
by A19, MSSCYC_1:def 2;
hence
(((m + 1),(len p)) -cut p) ^ ((1,m) -cut p) is
cyclic Path of
G
;
verum end; end;